English
If P is G2 embedded, then the sign of pairingIn i j agrees with the sign of pairingIn j i, i.e., lt comparisons reflect symmetry.
Русский
Если P встроено как G2, знак pairingIn i j совпадает со знаком pairingIn j i, то есть сравнения порядка сохраняют симметрию.
LaTeX
$$$ P.pairingIn S i j \lt 0 \iff P.pairingIn S j i \lt 0 $$$
Lean4
/-- For a reduced, crystallographic, irreducible root pairing other than `𝔤₂`, if the sum of two
roots is a root, they cannot make an acute angle.
To see that this lemma fails for `𝔤₂`, let `α` (short) and `β` (long) be a base. Then the roots
`α + β` and `2α + β` make an angle `π / 3` even though `3α + 2β` is a root. We can even witness as:
```lean
example (P : RootPairing ι R M N) [P.EmbeddedG2] :
P.pairingIn ℤ (EmbeddedG2.shortAddLong P) (EmbeddedG2.twoShortAddLong P) = 1 := by
simp
```
-/
theorem pairingIn_le_zero_of_root_add_mem [P.IsNotG2] (h : P.root i + P.root j ∈ range P.root) :
P.pairingIn ℤ i j ≤ 0 :=
by
have aux₁ := P.linearIndependent_of_add_mem_range_root' <| add_comm (P.root i) (P.root j) ▸ h
have aux₂ := P.chainBotCoeff_add_chainTopCoeff_le_two j i
have aux₃ : 1 ≤ P.chainTopCoeff j i := by rwa [← root_add_nsmul_mem_range_iff_le_chainTopCoeff aux₁, one_smul]
rw [← P.chainBotCoeff_sub_chainTopCoeff aux₁]
cutsat
