AF_coeff factorization: 4ζ₆ - 2 = 2·(2ζ₆ - 1)

def FUST.SpectralObstruction.two_zeta6_sub_one : FrourioAlgebra.GoldenEisensteinInt

Equations

• FUST.SpectralObstruction.two_zeta6_sub_one = { a := -1, b := 0, c := 2, d := 0 }

theorem FUST.SpectralObstruction.AF_coeff_factor_two : FrourioAlgebra.GoldenEisensteinInt.AF_coeff_gei = { a := 2, b := 0, c := 0, d := 0 }.mul two_zeta6_sub_one

theorem FUST.SpectralObstruction.two_zeta6_sub_one_sq : two_zeta6_sub_one.mul two_zeta6_sub_one = { a := -3, b := 0, c := 0, d := 0 }

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

1+ζ₆: the prime above 3

(1+ζ₆)·(2-ζ₆) = 3, so (1+ζ₆) is a prime of norm 9 in ℤ[φ,ζ₆].

def FUST.SpectralObstruction.one_plus_zeta6 : FrourioAlgebra.GoldenEisensteinInt

Equations

• FUST.SpectralObstruction.one_plus_zeta6 = { a := 1, b := 0, c := 1, d := 0 }

def FUST.SpectralObstruction.two_sub_zeta6 : FrourioAlgebra.GoldenEisensteinInt

Equations

• FUST.SpectralObstruction.two_sub_zeta6 = { a := 2, b := 0, c := -1, d := 0 }

theorem FUST.SpectralObstruction.tau_one_plus_zeta6 : one_plus_zeta6.tau = two_sub_zeta6

theorem FUST.SpectralObstruction.one_plus_zeta6_norm_three : one_plus_zeta6.mul two_sub_zeta6 = { a := 3, b := 0, c := 0, d := 0 }

theorem FUST.SpectralObstruction.one_plus_zeta6_tau_norm : one_plus_zeta6.mul one_plus_zeta6.tau = { a := 3, b := 0, c := 0, d := 0 }

theorem FUST.SpectralObstruction.one_plus_zeta6_fullNorm : one_plus_zeta6.norm = 9

SymNum coefficient: 6 = 2·3

def FUST.SpectralObstruction.sy_coeff : FrourioAlgebra.GoldenEisensteinInt

Equations

• FUST.SpectralObstruction.sy_coeff = { a := 6, b := 0, c := 0, d := 0 }

theorem FUST.SpectralObstruction.sy_coeff_factor_two : sy_coeff = { a := 2, b := 0, c := 0, d := 0 }.mul { a := 3, b := 0, c := 0, d := 0 }

Universal 2-divisibility: c_A·AF_coeff + c_S·6 is always even

theorem FUST.SpectralObstruction.eigenvalue_even (c_A c_S : ℤ) : ∃ (μ : FrourioAlgebra.GoldenEisensteinInt), ({ a := c_A, b := 0, c := 0, d := 0 }.mul FrourioAlgebra.GoldenEisensteinInt.AF_coeff_gei).add ({ a := c_S, b := 0, c := 0, d := 0 }.mul sy_coeff) = { a := 2, b := 0, c := 0, d := 0 }.mul μ

def FUST.SpectralObstruction.half_eigenvalue (c_A c_S : ℤ) : FrourioAlgebra.GoldenEisensteinInt

Equations

• FUST.SpectralObstruction.half_eigenvalue c_A c_S = ({ a := c_A, b := 0, c := 0, d := 0 }.mul FUST.SpectralObstruction.two_zeta6_sub_one).add { a := 3 * c_S, b := 0, c := 0, d := 0 }

theorem FUST.SpectralObstruction.half_eigenvalue_eq (c_A c_S : ℤ) : ({ a := c_A, b := 0, c := 0, d := 0 }.mul FrourioAlgebra.GoldenEisensteinInt.AF_coeff_gei).add ({ a := c_S, b := 0, c := 0, d := 0 }.mul sy_coeff) = { a := 2, b := 0, c := 0, d := 0 }.mul (half_eigenvalue c_A c_S)

theorem FUST.SpectralObstruction.half_eigenvalue_components (c_A c_S : ℤ) : half_eigenvalue c_A c_S = { a := -c_A + 3 * c_S, b := 0, c := 2 * c_A, d := 0 }

Mod 3 structure: μ = 2c_A·(1+ζ₆) + 3·q

theorem FUST.SpectralObstruction.half_eigenvalue_mod3 (c_A c_S : ℤ) : ∃ (q : FrourioAlgebra.GoldenEisensteinInt), half_eigenvalue c_A c_S = ({ a := 2 * c_A, b := 0, c := 0, d := 0 }.mul one_plus_zeta6).add ({ a := 3, b := 0, c := 0, d := 0 }.mul q)

5-divisibility: SY coefficients are always divisible by 5

theorem FUST.SpectralObstruction.sy_channel_ten_divisible (a b : ℤ) : { a := 6, b := 0, c := 0, d := 0 }.mul { a := 5 * a, b := 5 * b, c := 0, d := 0 } = { a := 10, b := 0, c := 0, d := 0 }.mul { a := 3 * a, b := 3 * b, c := 0, d := 0 }

Pairwise dark coupling: coprime-to-6 modes always couple to kernel

theorem FUST.SpectralObstruction.pairwise_sum_in_kernel (a b : ZMod 6) (ha : a = 1 ∨ a = 5) (hb : b = 1 ∨ b = 5) : ¬(a + b = 1 ∨ a + b = 5)

theorem FUST.SpectralObstruction.triple_sum_can_be_active : ∃ (a : ZMod 6) (b : ZMod 6) (c : ZMod 6), (a = 1 ∨ a = 5) ∧ (b = 1 ∨ b = 5) ∧ (c = 1 ∨ c = 5) ∧ (a + b + c = 1 ∨ a + b + c = 5)

theorem FUST.SpectralObstruction.triple_sum_not_always_active : ∃ (a : ZMod 6) (b : ZMod 6) (c : ZMod 6), (a = 1 ∨ a = 5) ∧ (b = 1 ∨ b = 5) ∧ (c = 1 ∨ c = 5) ∧ ¬(a + b + c = 1 ∨ a + b + c = 5)

Kernel fraction: 4/6 dark, 2/6 active

theorem FUST.SpectralObstruction.active_residues : {n : ZMod 6 | n = 1 ∨ n = 5}.card = 2

theorem FUST.SpectralObstruction.kernel_residues : {n : ZMod 6 | ¬(n = 1 ∨ n = 5)}.card = 4

Shadow lattice: φ, ζ₆, φζ₆ are unreachable from ℤ + 2·ℤ[φ,ζ₆]

theorem FUST.SpectralObstruction.phi_not_reachable : ¬∃ (k : ℤ) (μ : FrourioAlgebra.GoldenEisensteinInt), { a := k, b := 0, c := 0, d := 0 }.add ({ a := 2, b := 0, c := 0, d := 0 }.mul μ) = { a := 0, b := 1, c := 0, d := 0 }

theorem FUST.SpectralObstruction.zeta6_not_reachable : ¬∃ (k : ℤ) (μ : FrourioAlgebra.GoldenEisensteinInt), { a := k, b := 0, c := 0, d := 0 }.add ({ a := 2, b := 0, c := 0, d := 0 }.mul μ) = { a := 0, b := 0, c := 1, d := 0 }

theorem FUST.SpectralObstruction.phi_zeta6_not_reachable : ¬∃ (k : ℤ) (μ : FrourioAlgebra.GoldenEisensteinInt), { a := k, b := 0, c := 0, d := 0 }.add ({ a := 2, b := 0, c := 0, d := 0 }.mul μ) = { a := 0, b := 0, c := 0, d := 1 }

N(10·(1+ζ₆)) = 90000 = 2⁴·3²·5⁴

def FUST.SpectralObstruction.ten_one_plus_zeta6 : FrourioAlgebra.GoldenEisensteinInt

Equations

• FUST.SpectralObstruction.ten_one_plus_zeta6 = { a := 10, b := 0, c := 0, d := 0 }.mul FUST.SpectralObstruction.one_plus_zeta6

theorem FUST.SpectralObstruction.ten_one_plus_zeta6_eq : ten_one_plus_zeta6 = { a := 10, b := 0, c := 10, d := 0 }

theorem FUST.SpectralObstruction.obstruction_ideal_norm : ten_one_plus_zeta6.norm = 90000

theorem FUST.SpectralObstruction.norm_factorization : 90000 = 2 ^ 4 * 3 ^ 2 * 5 ^ 4

Three-layer factorization: 10·(1+ζ₆) = 2·5·(1+ζ₆)

theorem FUST.SpectralObstruction.obstruction_factorization : ten_one_plus_zeta6 = ({ a := 2, b := 0, c := 0, d := 0 }.mul { a := 5, b := 0, c := 0, d := 0 }).mul one_plus_zeta6

theorem FUST.SpectralObstruction.norm_decomposition : ten_one_plus_zeta6.norm = { a := 2, b := 0, c := 0, d := 0 }.norm * { a := 5, b := 0, c := 0, d := 0 }.norm * one_plus_zeta6.norm

theorem FUST.SpectralObstruction.norm_two : { a := 2, b := 0, c := 0, d := 0 }.norm = 16

theorem FUST.SpectralObstruction.norm_five : { a := 5, b := 0, c := 0, d := 0 }.norm = 625

theorem FUST.SpectralObstruction.euler_factor_product : 16 * 625 * 9 = 90000

Summary

theorem FUST.SpectralObstruction.obstruction_primes : { a := 2, b := 0, c := 0, d := 0 }.norm = 2 ^ 4 ∧ { a := 5, b := 0, c := 0, d := 0 }.norm = 5 ^ 4 ∧ one_plus_zeta6.norm = 3 ^ 2 ∧ ten_one_plus_zeta6.norm = 2 ^ 4 * 3 ^ 2 * 5 ^ 4