Galois Coarsening: Canonical Projections from ℤ[φ,ζ₆]

Fζ eigenvalues live in ℤ[φ,ζ₆] with Galois group Gal(ℚ(√5,√-3)/ℚ) ≅ (ℤ/2)². The three nontrivial Galois elements define canonical coarsening projections with NO free parameters:

• N_σ: ℤ[φ,ζ₆] → ℤ[ζ₆] (remove scale φ, keep gauge ζ₆)
• N_τ: ℤ[φ,ζ₆] → ℤ[φ] (remove gauge ζ₆, keep scale φ)
• N: ℤ[φ,ζ₆] → ℤ (remove both)

These are the UNIQUE coarsenings determined by the algebraic structure itself.

Eigenvalue dimension system in ℤ[φ,ζ₆]

Fζ eigenvalue = α(n)·AF_coeff + β(n) where α,β ∈ ℤ[φ], AF_coeff = -2+4ζ₆. Mass formula: |eigenvalue|² = β² + 12α² (AF_coeff = 2i√3).

def FUST.Coarsening.fromChannels (α β : FrourioAlgebra.GoldenInt) : FrourioAlgebra.GoldenEisensteinInt

Construct ℤ[φ,ζ₆] element from AF/SY channels: α·AF_coeff + β

Equations

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

theorem FUST.Coarsening.fromChannels_eq (α β : FrourioAlgebra.GoldenInt) : fromChannels α β = { a := β.a - 2 * α.a, b := β.b - 2 * α.b, c := 4 * α.a, d := 4 * α.b }

theorem FUST.Coarsening.fromChannels_zero : fromChannels { a := 0, b := 0 } { a := 0, b := 0 } = FrourioAlgebra.GoldenEisensteinInt.zero

def FUST.Coarsening.psiPowNat (n : ℕ) : FrourioAlgebra.GoldenInt

ψ^n in ℤ[φ] via Galois conjugation: ψ^n = conj(φ^n)

Equations

• FUST.Coarsening.psiPowNat n = (FUST.FrourioAlgebra.GoldenInt.phiPowNat n).conj

theorem FUST.Coarsening.psiPowNat_toReal (n : ℕ) : (psiPowNat n).toReal = ψ ^ n

psiPowNat n corresponds to ψ^n in ℝ

def FUST.Coarsening.phiA_goldenInt (n : ℕ) : FrourioAlgebra.GoldenInt

Φ_A eigenvalue on z^n in ℤ[φ]

Equations

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

def FUST.Coarsening.phiS_goldenInt (n : ℕ) : FrourioAlgebra.GoldenInt

Φ_S_int eigenvalue on z^n in ℤ[φ]

Equations

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

def FUST.Coarsening.eigenFζ_mod1 (k : ℕ) : FrourioAlgebra.GoldenEisensteinInt

Eigenvalue of Fζ on z^{6k+1} as ℤ[φ,ζ₆] element

Equations

• FUST.Coarsening.eigenFζ_mod1 k = FUST.Coarsening.fromChannels ({ a := 5, b := 0 } * FUST.Coarsening.phiA_goldenInt (6 * k + 1)) ({ a := 6, b := 0 } * FUST.Coarsening.phiS_goldenInt (6 * k + 1))

def FUST.Coarsening.eigenFζ_mod5 (k : ℕ) : FrourioAlgebra.GoldenEisensteinInt

Eigenvalue of Fζ on z^{6k+5}: AF sign flipped

Equations

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

theorem FUST.Coarsening.phiA_goldenInt_one : phiA_goldenInt 1 = { a := -2, b := 4 }

theorem FUST.Coarsening.phiS_goldenInt_one : phiS_goldenInt 1 = { a := -15, b := 10 }

Active/Kernel mode classification

def FUST.Coarsening.isActiveMode (n : ℕ) : Bool

Equations

• FUST.Coarsening.isActiveMode n = (n % 6 == 1 || n % 6 == 5)

def FUST.Coarsening.isKernelMode (n : ℕ) : Bool

Equations

• FUST.Coarsening.isKernelMode n = !FUST.Coarsening.isActiveMode n

Composite state multiplication

def FUST.Coarsening.compositeEigenvalue (x y : FrourioAlgebra.GoldenEisensteinInt) : FrourioAlgebra.GoldenEisensteinInt

Equations

• FUST.Coarsening.compositeEigenvalue x y = x.mul y

theorem FUST.Coarsening.AF_coeff_sq : FrourioAlgebra.GoldenEisensteinInt.AF_coeff_gei.mul FrourioAlgebra.GoldenEisensteinInt.AF_coeff_gei = { a := -12, b := 0, c := 0, d := 0 }

AF_coeff² = -12 in ℤ[ζ₆] ⊂ ℤ[φ,ζ₆]

theorem FUST.Coarsening.composite_channels (a1 b1 a2 b2 : FrourioAlgebra.GoldenInt) : compositeEigenvalue (fromChannels a1 b1) (fromChannels a2 b2) = fromChannels (a1 * b2 + a2 * b1) (b1 * b2 + { a := -12, b := 0 } * (a1 * a2))

theorem FUST.Coarsening.active_product_kernel (a b : ℕ) (ha : isActiveMode a = true) (hb : isActiveMode b = true) : isKernelMode (a + b) = true

τ-norm formula: |eigenvalue|² = β² + 12α²

noncomputable def FUST.Coarsening.tauNormSq (x : FrourioAlgebra.GoldenEisensteinInt) : ℝ

Equations

• FUST.Coarsening.tauNormSq x = Complex.normSq x.toComplex

theorem FUST.Coarsening.tauNormSq_formula (α β : FrourioAlgebra.GoldenInt) : tauNormSq (fromChannels α β) = β.toReal ^ 2 + 12 * α.toReal ^ 2

Bridge: Fζ evaluation ↔ GEI eigenvalue ↔ tauNormSq

theorem FUST.Coarsening.phiA_goldenInt_toReal (n : ℕ) : (phiA_goldenInt n).toReal = φ ^ (3 * n) - 4 * φ ^ (2 * n) + (3 + φ) * φ ^ n - (4 - φ) * ψ ^ n + 4 * ψ ^ (2 * n) - ψ ^ (3 * n)

theorem FUST.Coarsening.phiS_goldenInt_toReal (n : ℕ) : (phiS_goldenInt n).toReal = 10 * φ ^ (2 * n) + (21 - 2 * φ) * φ ^ n - 50 + (9 + 2 * φ) * ψ ^ n + 10 * ψ ^ (2 * n)

theorem FUST.Coarsening.Fζ_eigenvalue_bridge_mod1 (k : ℕ) : FζOperator.Fζ (fun (w : ℂ) => w ^ (6 * k + 1)) 1 = (eigenFζ_mod1 k).toComplex

Fζ(z^{6k+1})(1) = toComplex(eigenFζ_mod1 k)

theorem FUST.Coarsening.Fζ_eigenvalue_bridge_mod5 (k : ℕ) : FζOperator.Fζ (fun (w : ℂ) => w ^ (6 * k + 5)) 1 = (eigenFζ_mod5 k).toComplex

Fζ(z^{6k+5})(1) = toComplex(eigenFζ_mod5 k)

theorem FUST.Coarsening.Fζ_normSq_eq_tauNormSq_mod1 (k : ℕ) : Complex.normSq (FζOperator.Fζ (fun (w : ℂ) => w ^ (6 * k + 1)) 1) = tauNormSq (eigenFζ_mod1 k)

|Fζ(z^{6k+1})(1)|² = tauNormSq(eigenFζ_mod1 k)

theorem FUST.Coarsening.Fζ_normSq_eq_tauNormSq_mod5 (k : ℕ) : Complex.normSq (FζOperator.Fζ (fun (w : ℂ) => w ^ (6 * k + 5)) 1) = tauNormSq (eigenFζ_mod5 k)

|Fζ(z^{6k+5})(1)|² = tauNormSq(eigenFζ_mod5 k)

theorem FUST.Coarsening.emergence_tauNormSq_matter (j k : ℕ) : Complex.normSq (FζOperator.derivDefect (fun (w : ℂ) => w ^ (6 * j + 3)) (fun (w : ℂ) => w ^ (6 * k + 4)) 1) = tauNormSq (eigenFζ_mod1 (j + k + 1))

|δ(z^{6j+3}, z^{6k+4})(1)|² = tauNormSq (matter emergence)

theorem FUST.Coarsening.emergence_tauNormSq_antimatter (j k : ℕ) : Complex.normSq (FζOperator.derivDefect (fun (w : ℂ) => w ^ (6 * j + 2)) (fun (w : ℂ) => w ^ (6 * k + 3)) 1) = tauNormSq (eigenFζ_mod5 (j + k))

|δ(z^{6j+2}, z^{6k+3})(1)|² = tauNormSq (antimatter emergence)

theorem FUST.Coarsening.factorization_assoc (x y z : FrourioAlgebra.GoldenEisensteinInt) : compositeEigenvalue (compositeEigenvalue x y) z = compositeEigenvalue x (compositeEigenvalue y z)

theorem FUST.Coarsening.composite_comm (x y : FrourioAlgebra.GoldenEisensteinInt) : compositeEigenvalue x y = compositeEigenvalue y x

Eigenvalue for each active mode as ℤ[φ,ζ₆] element

def FUST.Coarsening.eigenGEI (n : ℕ) : FrourioAlgebra.GoldenEisensteinInt

Fζ eigenvalue for active mode n

Equations

• FUST.Coarsening.eigenGEI n = if n % 6 = 1 then FUST.Coarsening.eigenFζ_mod1 (n / 6) else if n % 6 = 5 then FUST.Coarsening.eigenFζ_mod5 (n / 6) else FUST.FrourioAlgebra.GoldenEisensteinInt.zero

theorem FUST.Coarsening.eigenGEI_kernel {n : ℕ} (h1 : n % 6 ≠ 1) (h5 : n % 6 ≠ 5) : eigenGEI n = FrourioAlgebra.GoldenEisensteinInt.zero

N_τ projection: ℤ[φ,ζ₆] → ℤ[φ] (remove gauge, keep scale)

def FUST.Coarsening.tauCoarsen (n : ℕ) : FrourioAlgebra.GoldenInt

τ-coarsening of mode n: eigenvalue projected to ℤ[φ]

Equations

• FUST.Coarsening.tauCoarsen n = (FUST.Coarsening.eigenGEI n).tauNorm

theorem FUST.Coarsening.tauCoarsen_kernel {n : ℕ} (h1 : n % 6 ≠ 1) (h5 : n % 6 ≠ 5) : tauCoarsen n = { a := 0, b := 0 }

N_σ projection: ℤ[φ,ζ₆] → ℤ[ζ₆] (remove scale, keep gauge)

def FUST.Coarsening.sigmaCoarsen (n : ℕ) : ℤ × ℤ

σ-coarsening of mode n: eigenvalue projected to ℤ[ζ₆] as (p, q) = p + q·ζ₆

Equations

• FUST.Coarsening.sigmaCoarsen n = (FUST.Coarsening.eigenGEI n).sigmaNorm

theorem FUST.Coarsening.sigmaCoarsen_kernel {n : ℕ} (h1 : n % 6 ≠ 1) (h5 : n % 6 ≠ 5) : sigmaCoarsen n = (0, 0)

Full norm N: ℤ[φ,ζ₆] → ℤ (remove all structure)

def FUST.Coarsening.fullNorm (n : ℕ) : ℤ

Full Galois norm of mode n

Equations

• FUST.Coarsening.fullNorm n = (FUST.Coarsening.eigenGEI n).norm

theorem FUST.Coarsening.fullNorm_kernel {n : ℕ} (h1 : n % 6 ≠ 1) (h5 : n % 6 ≠ 5) : fullNorm n = 0

N_τ preserves τ-norm: |λ|² = toReal(N_τ(λ))

noncomputable def FUST.Coarsening.eigenNormSq (n : ℕ) : ℝ

Equations

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

theorem FUST.Coarsening.eigenNormSq_nonneg (n : ℕ) : 0 ≤ eigenNormSq n

Coarsening on spectral coefficients

noncomputable def FUST.Coarsening.coarsenTau (c : ℕ → ℂ) : ℕ → ℂ

Apply τ-coarsening to spectrum: project each eigenvalue to ℤ[φ]

Equations

• FUST.Coarsening.coarsenTau c n = if FUST.Coarsening.isActiveMode n = true then c n * ↑(FUST.Coarsening.tauCoarsen n).toReal else 0

noncomputable def FUST.Coarsening.coarsenSigma (c : ℕ → ℂ) : ℕ → ℂ

Apply σ-coarsening to spectrum: project each eigenvalue to ℤ[ζ₆]

Equations

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

def FUST.Coarsening.coarsenFull (c : ℕ → ℂ) : ℕ → ℂ

Apply full norm coarsening: project each eigenvalue to ℤ

Equations

• FUST.Coarsening.coarsenFull c n = if FUST.Coarsening.isActiveMode n = true then c n * ↑(FUST.Coarsening.fullNorm n) else 0

Kernel preservation

theorem FUST.Coarsening.coarsenTau_kernel (c : ℕ → ℂ) {n : ℕ} (h : isActiveMode n = false) : coarsenTau c n = 0

theorem FUST.Coarsening.coarsenFull_kernel (c : ℕ → ℂ) {n : ℕ} (h : isActiveMode n = false) : coarsenFull c n = 0

Linearity

theorem FUST.Coarsening.coarsenTau_add (c₁ c₂ : ℕ → ℂ) : (coarsenTau fun (n : ℕ) => c₁ n + c₂ n) = fun (n : ℕ) => coarsenTau c₁ n + coarsenTau c₂ n

theorem FUST.Coarsening.coarsenFull_add (c₁ c₂ : ℕ → ℂ) : (coarsenFull fun (n : ℕ) => c₁ n + c₂ n) = fun (n : ℕ) => coarsenFull c₁ n + coarsenFull c₂ n

theorem FUST.Coarsening.coarsenTau_smul (a : ℂ) (c : ℕ → ℂ) : (coarsenTau fun (n : ℕ) => a * c n) = fun (n : ℕ) => a * coarsenTau c n

theorem FUST.Coarsening.coarsenFull_smul (a : ℂ) (c : ℕ → ℂ) : (coarsenFull fun (n : ℕ) => a * c n) = fun (n : ℕ) => a * coarsenFull c n

Galois coarsening hierarchy

The three projections form a commutative diagram: ℤ[φ,ζ₆] --N_σ--> ℤ[ζ₆] | | N_τ N_{ℤ[ζ₆]} | | v v ℤ[φ] --N_{ℤ[φ]}--> ℤ

Spectral decomposition: N_τ = 36·Φ_S² + 300·Φ_A²

theorem FUST.Coarsening.tauNorm_fromChannels (α β : FrourioAlgebra.GoldenInt) : (fromChannels α β).tauNorm = β * β + { a := 12, b := 0 } * (α * α)

theorem FUST.Coarsening.tauCoarsen_decomp_mod1 (k : ℕ) : tauCoarsen (6 * k + 1) = { a := 36, b := 0 } * (phiS_goldenInt (6 * k + 1) * phiS_goldenInt (6 * k + 1)) + { a := 300, b := 0 } * (phiA_goldenInt (6 * k + 1) * phiA_goldenInt (6 * k + 1))

theorem FUST.Coarsening.tauCoarsen_decomp_mod5 (k : ℕ) : tauCoarsen (6 * k + 5) = { a := 36, b := 0 } * (phiS_goldenInt (6 * k + 5) * phiS_goldenInt (6 * k + 5)) + { a := 300, b := 0 } * (phiA_goldenInt (6 * k + 5) * phiA_goldenInt (6 * k + 5))

Φ_A(1) = 2√5 and Φ_A(1)² = 20

theorem FUST.Coarsening.phiA_sq_one : phiA_goldenInt 1 * phiA_goldenInt 1 = { a := 20, b := 0 }

theorem FUST.Coarsening.phiA_one_toReal : (phiA_goldenInt 1).toReal = 2 * √5

tauNormSq = toReal(tauNorm) bridge

theorem FUST.Coarsening.tauNormSq_eq_tauNorm_toReal (α β : FrourioAlgebra.GoldenInt) : tauNormSq (fromChannels α β) = (fromChannels α β).tauNorm.toReal

Poincaré Casimir decomposition: tauNormSq vs casimirMassSq

theorem FUST.Coarsening.phiS_eq_five_phiS_coeff (n : ℕ) : (phiS_goldenInt n).toReal = 5 * Physics.Gravity.Φ_S_coeff n

phiS_goldenInt.toReal = 5 · Φ_S_coeff

theorem FUST.Coarsening.phiA_eq_temporal (n : ℕ) : (phiA_goldenInt n).toReal = Physics.Gravity.Φ_A_coeff n

phiA_goldenInt equals temporal Dζ component

theorem FUST.Coarsening.eigenNormSq_decomp_mod1 (k : ℕ) : eigenNormSq (6 * k + 1) = 900 * Physics.Gravity.Φ_S_coeff (6 * k + 1) ^ 2 + 300 * Physics.Gravity.Φ_A_coeff (6 * k + 1) ^ 2

eigenNormSq = 900·Φ_S² + 300·Φ_A²

theorem FUST.Coarsening.tauNormSq_casimir_relation_mod1 (k : ℕ) : eigenNormSq (6 * k + 1) = 25 * casimirMassSq (6 * k + 1) + 1800 * Physics.Gravity.Φ_S_coeff (6 * k + 1) ^ 2

tauNormSq = 25·casimirMassSq + 1800·Φ_S²