Root strings in the pinned F₄ root system

This file derives root-string bounds from the invariant root-length identity. The proofs use the abstract root-system API after the pinned length table has supplied the two possible squared lengths. They avoid case splits over the forty-eight root coordinates.

The initial results cover the strings needed to construct the characteristic-two short-root submodule. In particular, a short-short bracket landing in a long root has absolute structure constant two, while a long-root direction preserves the short-root span.

noncomputable def TauCeti.DynkinType.f4OppositeRootIndex (α : Fin 48) : Fin 48

The pinned index of the root opposite to α.

Equations

• TauCeti.DynkinType.f4OppositeRootIndex α = (TauCeti.DynkinType.f4SimplyConnectedRootDatum.reflectionPerm α) α

theorem TauCeti.DynkinType.f4OppositeRootIndex_eq_reflectionPerm (α : Fin 48) : f4OppositeRootIndex α = (f4SimplyConnectedRootDatum.reflectionPerm α) α

The opposite index is the self-reflection in the pinned root datum.

@[simp]

theorem TauCeti.DynkinType.f4OppositeRootIndex_f4OppositeRootIndex (α : Fin 48) : f4OppositeRootIndex (f4OppositeRootIndex α) = α

Taking the opposite pinned root index twice restores the index.

theorem TauCeti.DynkinType.ne_f4OppositeRootIndex_comm (α β : Fin 48) : β ≠ f4OppositeRootIndex α ↔ α ≠ f4OppositeRootIndex β

Being non-opposite is symmetric in the two pinned root indices.

theorem TauCeti.DynkinType.f4Length_of_root_eq_add_zsmul (α β γ : Fin 48) (n : ℤ) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + n • f4SimplyConnectedRootDatum.root α) : f4Length γ = f4Length β + n * f4Length α * RootPairing.pairing f4SimplyConnectedRootDatum β α + n ^ 2 * f4Length α

The tabulated F4 root length is quadratic along every integral root relation.

theorem TauCeti.DynkinType.f4Length_opposite (α : Fin 48) : f4Length (f4OppositeRootIndex α) = f4Length α

Opposite pinned roots have the same squared length.

theorem TauCeti.DynkinType.f4_not_root_eq_add_nsmul_of_length_eq_of_two_le (α β γ : Fin 48) (n : ℕ) (hαβ : f4Length α = f4Length β) (hneg : f4SimplyConnectedRootDatum.root β ≠ -f4SimplyConnectedRootDatum.root α) (hn : 2 ≤ n) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + ↑n • f4SimplyConnectedRootDatum.root α) : False

An equal-length, non-opposite F4 root string has no second positive endpoint.

theorem TauCeti.DynkinType.f4_pairing_eq_zero_of_short_add_short_eq_long (α β γ : Fin 48) (hα : f4Length α = 1) (hβ : f4Length β = 1) (hγ : f4Length γ = 2) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root α) : RootPairing.pairing f4SimplyConnectedRootDatum β α = 0

When the sum of two short F4 roots is long, their Cartan pairing is zero.

theorem TauCeti.DynkinType.f4_n_eq_one_and_pairing_eq_neg_one_and_length_eq_one_of_short_add_nsmul_long (α β γ : Fin 48) (n : ℕ) (hα : f4Length α = 2) (hβ : f4Length β = 1) (hn : 0 < n) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + ↑n • f4SimplyConnectedRootDatum.root α) : n = 1 ∧ RootPairing.pairing f4SimplyConnectedRootDatum β α = -1 ∧ f4Length γ = 1

A positive root string from a short root in a long-root direction has at most one step, and that step is again short.

theorem TauCeti.DynkinType.f4_chainBotCoeff_eq_one_of_short_add_short_eq_long (α β γ : Fin 48) (hα : f4Length α = 1) (hβ : f4Length β = 1) (hγ : f4Length γ = 2) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root α) : RootPairing.chainBotCoeff α β = 1

The short-short-to-long root edge has descending chain coefficient one, so its Chevalley bracket coefficient has absolute value two.

theorem TauCeti.DynkinType.f4_pairings_of_long_add_two_short (α β γ : Fin 48) (hα : f4Length α = 1) (hβ : f4Length β = 2) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + 2 • f4SimplyConnectedRootDatum.root α) : RootPairing.pairing f4SimplyConnectedRootDatum β α = -2 ∧ RootPairing.pairing f4SimplyConnectedRootDatum α β = -1 ∧ f4Length γ = 2

If two steps in a short-root direction carry a long root to another root, the Cartan pairings are -2 and -1, and the endpoint is long. This is the root string underlying the quadratic term in the characteristic-two special isogeny.

theorem TauCeti.DynkinType.exists_f4_short_midpoint_of_long_add_two_short (α β γ : Fin 48) (hα : f4Length α = 1) (hβ : f4Length β = 2) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + 2 • f4SimplyConnectedRootDatum.root α) : ∃ (δ : Fin 48), f4SimplyConnectedRootDatum.root δ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root α ∧ f4Length δ = 1 ∧ RootPairing.chainBotCoeff α β = 0 ∧ RootPairing.chainTopCoeff α β = 2 ∧ RootPairing.chainBotCoeff α δ = 1 ∧ RootPairing.chainTopCoeff α δ = 1

A long root and a short direction joined by a two-step root string have descending coefficient zero and ascending coefficient two. The intermediate root is short, and its outgoing bracket coefficient has absolute value two.

theorem TauCeti.DynkinType.f4_chainBotCoeff_eq_zero_of_add_of_length_eq (α β γ : Fin 48) (hβγ : f4Length β = f4Length γ) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root α) : RootPairing.chainBotCoeff α β = 0

An F4 root edge whose source and target have equal length has descending chain coefficient zero, regardless of the length of the root direction.

theorem TauCeti.DynkinType.f4Length_eq_two_of_root_eq_add_of_long_long (α β γ : Fin 48) (hα : f4Length α = 2) (hβ : f4Length β = 2) (hγ : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root α) : f4Length γ = 2

The sum of two long roots, when it is a root, is long.

theorem TauCeti.DynkinType.f4_not_root_eq_long_add_three_short (α β γ : Fin 48) (hα : f4Length α = 1) (hβ : f4Length β = 2) (hγ : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + 3 • f4SimplyConnectedRootDatum.root α) : False

A short-root direction has no third step from a long root.

theorem TauCeti.DynkinType.f4_chainTopCoeff_eq_zero_of_short_pairing_eq_one (α β : Fin 48) (hβ : f4Length β = 1) (hpair : RootPairing.pairing f4SimplyConnectedRootDatum β α = 1) : RootPairing.chainTopCoeff α β = 0

A short root with Cartan pairing one has no positive step in the given root direction.

theorem TauCeti.DynkinType.f4_chainTopCoeff_eq_zero_of_short_long_pairing_eq_zero (α β : Fin 48) (hα : f4Length α = 2) (hβ : f4Length β = 1) (hpair : RootPairing.pairing f4SimplyConnectedRootDatum β α = 0) : RootPairing.chainTopCoeff α β = 0

A short root orthogonal to a long root has no positive step in the long-root direction.