English
If P is G2 embedded, then the values of pairingIn for certain indices i and j attain the set {−3, −1, 0, 1, 3}, under given nondegeneracy assumptions.
Русский
Если P встроено как G2, то значения pairingIn для некоторых индексов i и j достигают множества {−3, −1, 0, 1, 3} при заданных предположениях невырождения.
LaTeX
$$$ P.pairingIn\mathbb{Z} i j \in \{-3,-1,0,1,3\}$$$
Lean4
theorem pairingIn_mem_zero_one_three [P.IsG2] (i j : ι) (h : P.root i ≠ P.root j) (h' : P.root i ≠ -P.root j) :
P.pairingIn ℤ i j ∈ ({-3, -1, 0, 1, 3} : Set ℤ) :=
by
suffices
¬(∀ i j,
P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j)
by
have aux₁ := P.forall_pairingIn_eq_swap_or.resolve_left this i j
have aux₂ := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' i j h h'
simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_zero_zero, Prod.mk_eq_zero, Prod.mk_one_one, Prod.mk_eq_one,
Prod.mk.injEq] at aux₂ ⊢
cutsat
obtain ⟨k, l, hkl⟩ := exists_pairingIn_neg_three (P := P)
push_neg
refine ⟨k, l, ?_⟩
have aux := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed k l
simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_zero_zero, Prod.mk_eq_zero, Prod.mk_one_one, Prod.mk_eq_one,
Prod.mk.injEq] at aux
omega
