A₂ root system from Eisenstein integers

The ζ₆ sublattice ℤ[ζ₆] ⊂ ℤ[φ,ζ₆] has exactly 6 units: ±1, ±ζ₆, ±ζ₆². These form the A₂ root system with Cartan matrix [[2,-1],[-1,2]], which determines the Lie algebra su(3) (dim 8 = 6 roots + rank 2).

def FUST.cartanA2 : Matrix (Fin 2) (Fin 2) ℤ

Equations

• FUST.cartanA2 = !![2, -1; -1, 2]

theorem FUST.cartanA2_det : cartanA2.det = 3

def FUST.eisensteinUnits : Fin 6 → FrourioAlgebra.GoldenEisensteinInt

Equations

• One or more equations did not get rendered due to their size.

theorem FUST.eisensteinUnit_in_zeta6_sublattice (i : Fin 6) : (eisensteinUnits i).b = 0 ∧ (eisensteinUnits i).d = 0

theorem FUST.eisensteinUnit_isUnit (i : Fin 6) : (eisensteinUnits i).mul (eisensteinUnits i).tau = FrourioAlgebra.GoldenEisensteinInt.one

theorem FUST.eisenstein_norm_eq (a c : ℤ) : { a := a, b := 0, c := c, d := 0 }.norm = (a ^ 2 + a * c + c ^ 2) ^ 2

Eisenstein norm: for x in ℤ[ζ₆] sublattice (b=d=0), N(x) = (a²+ac+c²)²

theorem FUST.eisenstein_unit_classification (a c : ℤ) (h : a ^ 2 + a * c + c ^ 2 = 1) : a = 1 ∧ c = 0 ∨ a = 0 ∧ c = 1 ∨ a = -1 ∧ c = 1 ∨ a = -1 ∧ c = 0 ∨ a = 0 ∧ c = -1 ∨ a = 1 ∧ c = -1

Classification: a²+ac+c²=1 has exactly 6 integer solutions

theorem FUST.cartan_pairing_offdiag : 2 * (1 * (-1 / 2) + 0 * (√3 / 2)) / (-1 / 2 * (-1 / 2) + √3 / 2 * (√3 / 2)) = -1

theorem FUST.U1_gauge_uniqueness : (∀ (x : FrourioAlgebra.GoldenEisensteinInt), x.sigma = x ∧ x.tau = x ↔ x.b = 0 ∧ x.c = 0 ∧ x.d = 0) ∧ (∀ (c : ℂ), c ≠ 0 → ∀ (f g : ℂ → ℂ) (z : ℂ), FζOperator.derivDefect (fun (w : ℂ) => c * f w) (fun (w : ℂ) => c⁻¹ * g w) z = FζOperator.derivDefect f g z) ∧ (∀ (c : ℂ), (starRingEnd ℂ) c * c = 1 → c • 1 ∈ Matrix.unitaryGroup (Fin 1) ℂ) ∧ (∀ (c : ℂ), (c • 1).det = c ^ 1) ∧ (∀ M ∈ Matrix.specialUnitaryGroup (Fin 1) ℂ, M = 1) ∧ ∀ (x : FrourioAlgebra.GoldenEisensteinInt), x.sigma = x ∧ x.tau = x ∧ (x.mul x = FrourioAlgebra.GoldenEisensteinInt.one ∨ x.mul x.neg = FrourioAlgebra.GoldenEisensteinInt.one) → x = FrourioAlgebra.GoldenEisensteinInt.one ∨ x = FrourioAlgebra.GoldenEisensteinInt.one.neg

U(1) gauge group uniqueness for the trivial channel.

The trivial channel is the Galois-fixed subspace of ℤ[φ,ζ₆]:

• galois_fixed_iff: σ(x)=x ∧ τ(x)=x ↔ b=c=d=0 (1D over ℤ)
• On 1D: norm-preserving gauge = unitaryGroup (Fin 1) ℂ = U(1)
• SU(1) = {I} is trivial: no SU reduction, full gauge is U(1)
• derivDefect_const_gauge: scalar U(1) is exactly the gauge freedom

theorem FUST.SU2_gauge_uniqueness : FrourioAlgebra.GoldenEisensteinInt.AF_coeff_gei.tau = FrourioAlgebra.GoldenEisensteinInt.AF_coeff_gei.neg ∧ (∀ (x : FrourioAlgebra.GoldenEisensteinInt), x.tau.tau = x) ∧ (∀ (x y : FrourioAlgebra.GoldenEisensteinInt), (x.mul y).tau = x.tau.mul y.tau) ∧ FrourioAlgebra.GoldenEisensteinInt.AF_coeff_gei.mul FrourioAlgebra.GoldenEisensteinInt.AF_coeff_gei = { a := -12, b := 0, c := 0, d := 0 } ∧ DζOperator.AF_coeff.im ≠ 0 ∧ (∀ (c : ℂ), (starRingEnd ℂ) c * c = 1 → c • 1 ∈ Matrix.unitaryGroup (Fin 2) ℂ) ∧ ∀ (c : ℂ), (c • 1).det = c ^ 2

SU(2) gauge group uniqueness for the AF channel.

The AF channel carries a quaternionic structure from τ-anti-invariance:

• τ(AF_coeff) = -AF_coeff and τ² = id give eigenvalue -1
• AF_coeff² = -12: the J² < 0 quaternionic condition
• The 1D-over-ℂ AF space with quaternionic doubling gives ℂ² = ℍ¹
• Norm preservation on ℂ² → U(2), scalar separation → SU(2) = Sp(1)

theorem FUST.SU3_gauge_uniqueness : cartanA2.det = 3 ∧ (∀ (a c : ℤ), a ^ 2 + a * c + c ^ 2 = 1 → a = 1 ∧ c = 0 ∨ a = 0 ∧ c = 1 ∨ a = -1 ∧ c = 1 ∨ a = -1 ∧ c = 0 ∨ a = 0 ∧ c = -1 ∨ a = 1 ∧ c = -1) ∧ (6 + 2 = 8 ∧ 3 ^ 2 - 1 = 8) ∧ starRingEnd ℂ ≠ RingHom.id ℂ ∧ ∀ (c : ℂ), c ≠ 0 → ∀ (f g : ℂ → ℂ) (z : ℂ), FζOperator.derivDefect (fun (w : ℂ) => c * f w) (fun (w : ℂ) => c⁻¹ * g w) z = FζOperator.derivDefect f g z

SU(3) gauge group from A₂ root system.

ℤ[ζ₆] has 6 units forming the A₂ root system (Cartan matrix [[2,-1],[-1,2]]). A₂ determines su(3): dim = 6 roots + rank 2 = 8 = 3²-1. Scalar U(1) separated by derivDefect, star≠id excludes SO.