English
If P is crystallographic, there exists at least one index i in ι (i.e., ι is nonempty) under IsG2 context.
Русский
Если P кристаллическое, то множество индексов ι непусто (существует i ∈ ι).
LaTeX
$$$ \exists i : ι, True $$$
Lean4
/-- For a reduced, crystallographic, irreducible root pairing other than `𝔤₂`, if the sum of two
roots is a root, the bottom chain coefficient is either one or zero according to whether they are
perpendicular.
To see that this lemma fails for `𝔤₂`, let `α` (short) and `β` (long) be a base. Then the roots
`α` and `α + β` provide a counterexample. -/
theorem chainBotCoeff_if_one_zero [P.IsNotG2] (h : P.root i + P.root j ∈ range P.root) :
P.chainBotCoeff i j = if P.pairingIn ℤ i j = 0 then 1 else 0 :=
by
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
have aux₁ := P.linearIndependent_of_add_mem_range_root' h
have aux₂ := P.chainBotCoeff_add_chainTopCoeff_le_two i j
have aux₃ : 1 ≤ P.chainTopCoeff i j := P.one_le_chainTopCoeff_of_root_add_mem h
rcases eq_or_ne (P.chainBotCoeff i j) (P.chainTopCoeff i j) with aux₄ | aux₄ <;>
simp_rw [P.pairingIn_eq_zero_iff (i := i) (j := j), ← P.chainBotCoeff_sub_chainTopCoeff aux₁, sub_eq_zero,
Nat.cast_inj, aux₄, reduceIte] <;>
omega
