SY channel integrality: Re(λ) ∈ ℤ[φ]

The SY eigenvalue channel uses only φ and ψ (golden ratio roots). (6-2φ)·√5 = (6-2φ)(2φ-1) = 10φ - 10 clears denominators.

theorem FUST.SpectralGalois.phiS_int_coeff_real (n : ℕ) : 10 * φ ^ (2 * n) + (21 - 2 * φ) * φ ^ n - 50 + (9 + 2 * φ) * ψ ^ n + 10 * ψ ^ (2 * n) = 10 * FibonacciArithmetic.lucasConst (2 * n) + 15 * FibonacciArithmetic.lucasConst n + (6 - 2 * φ) * (φ ^ n - ψ ^ n) - 50

Φ_S_int = 10L_{2n} + 15L_n + (6-2φ)(φⁿ-ψⁿ) - 50

theorem FUST.SpectralGalois.phiS_int_fibonacci (n : ℕ) : 10 * φ ^ (2 * n) + (21 - 2 * φ) * φ ^ n - 50 + (9 + 2 * φ) * ψ ^ n + 10 * ψ ^ (2 * n) = 10 * FibonacciArithmetic.lucasConst (2 * n) + 15 * FibonacciArithmetic.lucasConst n - 50 + (6 - 2 * φ) * √5 * ↑(Nat.fib n)

Φ_S_int via Fibonacci: uses (6-2φ) = (5-√5) and (φⁿ-ψⁿ) = √5·F_n

theorem FUST.SpectralGalois.six_sub_two_phi_sqrt5 : (6 - 2 * φ) * (2 * φ - 1) = 10 * φ - 10

(6-2φ)·(2φ-1) = 10φ-10

theorem FUST.SpectralGalois.six_sub_two_phi_mul_sqrt5 : (6 - 2 * φ) * √5 = 10 * φ - 10

(6-2φ)·√5 = 10φ-10 via √5 = 2φ-1

theorem FUST.SpectralGalois.SY_coeff_golden_form (n : ℕ) : 10 * φ ^ (2 * n) + (21 - 2 * φ) * φ ^ n - 50 + (9 + 2 * φ) * ψ ^ n + 10 * ψ ^ (2 * n) = 10 * FibonacciArithmetic.lucasConst (2 * n) + 15 * FibonacciArithmetic.lucasConst n - 50 + (10 * φ - 10) * ↑(Nat.fib n)

SY coefficient decomposes as a + b·φ for a,b ∈ ℤ

Galois separation: eigenvalue lies in ℚ(√5) + ℚ(√5)·i√3

Each eigenvalue decomposes as Re(λ) ∈ ℤ[φ] + Im(λ)·i where Im ∝ √15. No √(-3) component on the real axis.

theorem FUST.SpectralGalois.galois_separation_re (c_A c_S : ℝ) : (5 * ↑(√5 * c_A) * DζOperator.AF_coeff + 6 * ↑c_S).re = 6 * c_S

AF channel has zero real part

theorem FUST.SpectralGalois.galois_separation_im (c_A c_S : ℝ) : (5 * ↑(√5 * c_A) * DζOperator.AF_coeff + 6 * ↑c_S).im = 10 * √15 * c_A

SY channel has zero imaginary part

theorem FUST.SpectralGalois.eigenvalue_from_channels (c_A c_S : ℝ) : 5 * ↑(√5 * c_A) * DζOperator.AF_coeff + 6 * ↑c_S = { re := 6 * c_S, im := 10 * √15 * c_A }

Eigenvalue channels determine the complex number

σ-conjugate: φ ↦ ψ, preserves ζ₆

σ maps √5 → -√5, so AF coefficient c_A sign-flips.

theorem FUST.SpectralGalois.sigma_im_flip (c_A c_S : ℝ) : (5 * ↑(√5 * -c_A) * DζOperator.AF_coeff + 6 * ↑c_S).im = -(10 * √15 * c_A)

σ-conjugate has negated AF coefficient

theorem FUST.SpectralGalois.sigma_re_preserved (c_A c_S : ℝ) : (5 * ↑(√5 * -c_A) * DζOperator.AF_coeff + 6 * ↑c_S).re = 6 * c_S

σ-conjugate preserves SY channel

theorem FUST.SpectralGalois.sigma_eigenvalue_form (c_A c_S : ℝ) : 5 * ↑(√5 * -c_A) * DζOperator.AF_coeff + 6 * ↑c_S = { re := 6 * c_S, im := -(10 * √15 * c_A) }

σ-conjugate as explicit complex number

τ-conjugate = complex conjugation

τ: ζ₆ ↦ 1-ζ₆ is complex conjugation.

theorem FUST.SpectralGalois.tau_is_conj (c_A c_S : ℝ) : (starRingEnd ℂ) (5 * ↑(√5 * c_A) * DζOperator.AF_coeff + 6 * ↑c_S) = { re := 6 * c_S, im := -(10 * √15 * c_A) }

τ acts as complex conjugation on eigenvalues

theorem FUST.SpectralGalois.tau_eigenvalue_eq (c_A c_S : ℝ) : (starRingEnd ℂ) (5 * ↑(√5 * c_A) * DζOperator.AF_coeff + 6 * ↑c_S) = 5 * ↑(√5 * -c_A) * DζOperator.AF_coeff + 6 * ↑c_S

τ-conjugate equals sign-flipped AF channel

Galois orbit structure

Gal(K/ℚ) = {id, σ, τ, στ}: id(λ) = ⟨6c_S, 10√15·c_A⟩, τ(λ) = ⟨6c_S, -10√15·c_A⟩, σ(λ) = ⟨6σ(c_S), -10√15·c_A⟩, στ(λ) = ⟨6σ(c_S), 10√15·c_A⟩

theorem FUST.SpectralGalois.galois_trace_rational (c_A c_S : ℝ) : 5 * ↑(√5 * c_A) * DζOperator.AF_coeff + 6 * ↑c_S + (starRingEnd ℂ) (5 * ↑(√5 * c_A) * DζOperator.AF_coeff + 6 * ↑c_S) = ↑(12 * c_S)

Galois trace: λ + conj(λ) = 12·c_S (AF cancels)

theorem FUST.SpectralGalois.tau_norm_eq_abs_sq (c_A c_S : ℝ) : (5 * ↑(√5 * c_A) * DζOperator.AF_coeff + 6 * ↑c_S) * (starRingEnd ℂ) (5 * ↑(√5 * c_A) * DζOperator.AF_coeff + 6 * ↑c_S) = { re := 36 * c_S ^ 2 + 1500 * c_A ^ 2, im := 0 }

τ-norm = |λ|²: 36c_S² + 1500c_A²

theorem FUST.SpectralGalois.abs_sq_pos (c_A c_S : ℝ) (h : c_A ≠ 0 ∨ c_S ≠ 0) : 36 * c_S ^ 2 + 1500 * c_A ^ 2 > 0

|λ|² is positive when c_A ≠ 0 or c_S ≠ 0

Missing √(-3) direction: the c=0 constraint

In the field basis {1, √5, √(-3), √(-15)}, eigenvalues have form λ = a + b√5 + 0·√(-3) + d·√(-15). The √(-3) coefficient is zero.

theorem FUST.SpectralGalois.no_sqrt_neg3_component (c_A c_S : ℝ) : ∃ (re_part : ℝ) (im_coeff : ℝ), 5 * ↑(√5 * c_A) * DζOperator.AF_coeff + 6 * ↑c_S = { re := re_part, im := im_coeff * √15 }

Eigenvalue has no √(-3) component: Im(λ) is ∝ √15

theorem FUST.SpectralGalois.norm_sq_formula (c_A c_S : ℝ) : Complex.normSq (5 * ↑(√5 * c_A) * DζOperator.AF_coeff + 6 * ↑c_S) = 36 * c_S ^ 2 + 1500 * c_A ^ 2

Eigenvalue normSq = 36c_S² + 1500c_A²

Separation principle: AF and SY are independent conditions

theorem FUST.SpectralGalois.SY_zero_pure_AF (c_A : ℝ) : 5 * ↑(√5 * c_A) * DζOperator.AF_coeff + 6 * 0 = { re := 0, im := 10 * √15 * c_A }

When SY vanishes, eigenvalue is pure AF

theorem FUST.SpectralGalois.AF_zero_pure_SY (c_S : ℝ) : 5 * ↑(√5 * 0) * DζOperator.AF_coeff + 6 * ↑c_S = ↑(6 * c_S)

When AF vanishes, eigenvalue is pure SY

theorem FUST.SpectralGalois.eigenvalue_unique_decomp (z₁ z₂ : ℂ) (c_A₁ c_S₁ c_A₂ c_S₂ : ℝ) (h1 : z₁ = 5 * ↑(√5 * c_A₁) * DζOperator.AF_coeff + 6 * ↑c_S₁) (h2 : z₂ = 5 * ↑(√5 * c_A₂) * DζOperator.AF_coeff + 6 * ↑c_S₂) (heq : z₁ = z₂) : c_S₁ = c_S₂ ∧ c_A₁ = c_A₂

Eigenvalue = SY + AF decomposition is unique