chainBotCoeff_add_chainTopCoeff_le_two

English

For a non-G2 crystallographic RootPairing, the sum of the bottom and top chain coefficients is at most 2; equivalently, the combined chain contribution is bounded.

Русский

Для кристаллизационного, не-G2 RootPairing сумма нижних и верхних членов цепи не превосходит 2; иначе суммарный вклад цепи ограничен.

LaTeX

$$$ P.chainBotCoeff i j + P.chainTopCoeff i j \le 2 $$$

Lean4

theorem chainBotCoeff_add_chainTopCoeff_le_two [P.IsNotG2] : P.chainBotCoeff i j + P.chainTopCoeff i j ≤ 2 :=
  by
  by_cases h : LinearIndependent R ![P.root i, P.root j]
  swap; · simp [chainTopCoeff_of_not_linearIndependent, chainBotCoeff_of_not_linearIndependent, h]
  rw [← Int.ofNat_le, Nat.cast_add, Nat.cast_ofNat, chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx h]
  have := IsNotG2.pairingIn_mem_zero_one_two (P := P) (P.chainTopIdx i j) i
  aesop

Похожие утверждения