Section 1: Diff₆ Spectral Coefficients (ℕ → ℝ)

Diff₆(xⁿ) = Cₙ · x^{n-1} for n ≥ 3

The coefficient Cₙ encodes the spectral structure of Diff₆.

noncomputable def FUST.SpectralCoefficients.Diff6Coeff (n : ℕ) : ℝ

Coefficient C_n for Diff₆(x^n) = C_n · x^{n-1}

Equations

• FUST.SpectralCoefficients.Diff6Coeff n = FUST.φ ^ (3 * n) - 3 * FUST.φ ^ (2 * n) + FUST.φ ^ n - FUST.ψ ^ n + 3 * FUST.ψ ^ (2 * n) - FUST.ψ ^ (3 * n)

theorem FUST.SpectralCoefficients.Diff6Coeff_zero : Diff6Coeff 0 = 0

C_0 = 0 (constant annihilation)

theorem FUST.SpectralCoefficients.Diff6Coeff_one : Diff6Coeff 1 = 0

C_1 = 0 (linear annihilation)

theorem FUST.SpectralCoefficients.Diff6Coeff_two : Diff6Coeff 2 = 0

C_2 = 0 (quadratic annihilation)

theorem FUST.SpectralCoefficients.Diff6Coeff_three : Diff6Coeff 3 = 12 * √5

C_3 = 12√5 (first non-kernel coefficient)

theorem FUST.SpectralCoefficients.Diff6Coeff_fibonacci (n : ℕ) : Diff6Coeff n = √5 * (↑(Nat.fib (3 * n)) - 3 * ↑(Nat.fib (2 * n)) + ↑(Nat.fib n))

Diff6Coeff expressed via Fibonacci: C_n = √5 · (F_{3n} - 3F_{2n} + F_n)

theorem FUST.SpectralCoefficients.Diff6Coeff_three_ne_zero : Diff6Coeff 3 ≠ 0

C_3 = 12√5 ≠ 0

theorem FUST.SpectralCoefficients.sqrt5_gt_22 : √5 > 2.2

Helper: √5 > 2.2

theorem FUST.SpectralCoefficients.phi_gt_16 : φ > 1.6

Helper: φ > 1.6

theorem FUST.SpectralCoefficients.phi_cubed_gt_4 : φ ^ 3 > 4

Helper: φ^3 > 4

theorem FUST.SpectralCoefficients.phi_pow_mono {n m : ℕ} (h : m ≤ n) : φ ^ m ≤ φ ^ n

Helper: φ^n ≥ φ^m for n ≥ m

theorem FUST.SpectralCoefficients.phi_pow_gt_3 (n : ℕ) (hn : n ≥ 3) : φ ^ n > 3

Helper: φ^n > 3 for n ≥ 3

theorem FUST.SpectralCoefficients.phi_pow_6_gt_17 : φ ^ 6 > 17

Helper: φ^6 > 17

theorem FUST.SpectralCoefficients.fib_combination_pos (n : ℕ) (hn : n ≥ 3) : Nat.fib (3 * n) + Nat.fib n > 3 * Nat.fib (2 * n)

F_{3n} + F_n > 3·F_{2n} for n ≥ 3

theorem FUST.SpectralCoefficients.Diff6Coeff_ne_zero_of_ge_three (n : ℕ) (hn : n ≥ 3) : Diff6Coeff n ≠ 0

C_n ≠ 0 for n ≥ 3 (spectrum is non-trivial)

theorem FUST.SpectralCoefficients.Diff6Coeff_eq_zero_iff (n : ℕ) : Diff6Coeff n = 0 ↔ n ≤ 2

Kernel characterization: C_n = 0 iff n ≤ 2

Section 2: Factorization and Asymptotics

theorem FUST.SpectralCoefficients.Diff6Coeff_factored (n : ℕ) : Diff6Coeff n = (φ ^ n - ψ ^ n) * (φ ^ (2 * n) + ψ ^ (2 * n) + (-1) ^ n + 1 - 3 * (φ ^ n + ψ ^ n))

Diff6Coeff factorization: C_n = (φ^n - ψ^n) * (φ^{2n} + ψ^{2n} + (-1)^n + 1 - 3(φ^n + ψ^n))

theorem FUST.SpectralCoefficients.Diff6Coeff_asymptotic (n : ℕ) (hn : n ≥ 3) : ∃ C > 0, |Diff6Coeff n - φ ^ (3 * n)| ≤ C * φ ^ (2 * n)

For large n, C_n ~ φ^{3n} (dominant term)

Section 2.5: Spectral Weight and Triple Factorization

The spectral weight Q_n = φ^{2n} + ψ^{2n} + (-1)^n + 1 - 3(φ^n + ψ^n) is the second factor in C_n = (φ^n - ψ^n) · Q_n.

Key identity: Q_n = (φ^n + ψ^n)² - 3(φ^n + ψ^n) + 1 - (-1)^n

This gives parity-dependent factorization: n odd: Q_n = (φ^n+ψ^n - 1)(φ^n+ψ^n - 2) n even: Q_n = (φ^n+ψ^n)(φ^n+ψ^n - 3)

The three kernel zeros n ∈ {0,1,2} arise from three distinct mechanisms: n=0: φ^0 - ψ^0 = 0 (Fibonacci difference vanishes) n=1: φ+ψ - 1 = 0 (Lucas sum at threshold) n=2: φ²+ψ² - 3 = 0 (Lucas sum at identity level, even parity)

noncomputable def FUST.SpectralCoefficients.spectralWeight (n : ℕ) : ℝ

Spectral weight Q_n: the symmetric factor in C_n = (φ^n - ψ^n) · Q_n

Equations

• FUST.SpectralCoefficients.spectralWeight n = FUST.φ ^ (2 * n) + FUST.ψ ^ (2 * n) + (-1) ^ n + 1 - 3 * (FUST.φ ^ n + FUST.ψ ^ n)

theorem FUST.SpectralCoefficients.spectralWeight_via_sum (n : ℕ) : spectralWeight n = (φ ^ n + ψ ^ n) ^ 2 - 3 * (φ ^ n + ψ ^ n) + 1 - (-1) ^ n

Q_n = (φ^n+ψ^n)² - 3(φ^n+ψ^n) + 1 - (-1)^n

theorem FUST.SpectralCoefficients.spectralWeight_odd (n : ℕ) (hn : Odd n) : spectralWeight n = (φ ^ n + ψ ^ n - 1) * (φ ^ n + ψ ^ n - 2)

n odd: Q_n = (φ^n+ψ^n - 1)(φ^n+ψ^n - 2)

theorem FUST.SpectralCoefficients.spectralWeight_even (n : ℕ) (hn : Even n) : spectralWeight n = (φ ^ n + ψ ^ n) * (φ ^ n + ψ ^ n - 3)

n even: Q_n = (φ^n+ψ^n)(φ^n+ψ^n - 3)

theorem FUST.SpectralCoefficients.Diff6Coeff_odd_factored (n : ℕ) (hn : Odd n) : Diff6Coeff n = (φ ^ n - ψ ^ n) * (φ ^ n + ψ ^ n - 1) * (φ ^ n + ψ ^ n - 2)

Triple factorization (odd): C_n = (φ^n-ψ^n)(φ^n+ψ^n-1)(φ^n+ψ^n-2)

theorem FUST.SpectralCoefficients.Diff6Coeff_even_factored (n : ℕ) (hn : Even n) : Diff6Coeff n = (φ ^ n - ψ ^ n) * (φ ^ n + ψ ^ n) * (φ ^ n + ψ ^ n - 3)

Triple factorization (even): C_n = (φ^n-ψ^n)(φ^n+ψ^n)(φ^n+ψ^n-3)

theorem FUST.SpectralCoefficients.Diff6_kernel_three_mechanisms : φ ^ 0 - ψ ^ 0 = 0 ∧ φ ^ 1 + ψ ^ 1 - 1 = 0 ∧ φ ^ 2 + ψ ^ 2 - 3 = 0

Three distinct zero mechanisms for dim ker(Diff₆) = 3

theorem FUST.SpectralCoefficients.spectralWeight_zero : spectralWeight 0 = -2

Q_0 = -2

theorem FUST.SpectralCoefficients.spectralWeight_one : spectralWeight 1 = 0

Q_1 = 0 (kernel: φ+ψ = 1)

theorem FUST.SpectralCoefficients.spectralWeight_two : spectralWeight 2 = 0

Q_2 = 0 (kernel: φ²+ψ² = 3)

theorem FUST.SpectralCoefficients.spectralWeight_three : spectralWeight 3 = 6

Q_3 = 6 (first non-zero spectral weight)

theorem FUST.SpectralCoefficients.Diff6Coeff_three_via_triple : Diff6Coeff 3 = (φ ^ 3 - ψ ^ 3) * (φ ^ 3 + ψ ^ 3 - 1) * (φ ^ 3 + ψ ^ 3 - 2)

C_3 = 2√5 · 3 · 2 = 12√5 via triple factorization

theorem FUST.SpectralCoefficients.spectralEigenvalue_factored (n : ℕ) : Diff6Coeff n = (φ ^ n - ψ ^ n) * spectralWeight n

Spectral eigenvalue via Fibonacci and spectral weight: λ_n = (φ^n-ψ^n) · Q_n / (√5)^5 = F_n · Q_n / (√5)^4 = F_n · Q_n / 25

Section 2.7: Fibonacci-Prime Bridge

The Diff6 spectral coefficient C_n = √5 · F_n · Q_n connects to prime numbers through the Fibonacci divisibility structure:

1. Binet: φ^n - ψ^n = √5 · F_n, so C_n = √5 · F_n · Q_n
2. Strong divisibility: gcd(F_m, F_n) = F_{gcd(m,n)} (Mathlib: Nat.fib_gcd)
3. Rank of apparition: every prime p divides F_{α(p)} where α(p) | p-(5/p)
4. Periodicity: p | F_{α(p)} | F_{k·α(p)} for all k ≥ 1

This means every prime p is encoded in the Diff6 spectrum: p | F_{α(p)}, so p | C_{α(p)} / (√5 · Q_{α(p)}) and p | C_{k·α(p)} / (√5 · Q_{k·α(p)}) for all k

The algebraic mechanism: p | F_n ⟺ φ^n ≡ ψ^n (mod p) in 𝔽_p[√5]. This is governed by the Frobenius element of ℚ(√5)/ℚ at p, connecting Diff6 (which lives in ℚ(√5)) to the Euler product of ζ(s).

Key factorization: ζ_{ℚ(√5)}(s) = ζ(s) · L(s, χ_5) where χ_5 is the Kronecker symbol (5/·).

theorem FUST.SpectralCoefficients.fib_binet (n : ℕ) : ↑(Nat.fib n) = (φ ^ n - ψ ^ n) / √5

Binet formula: F_n = (φ^n - ψ^n) / √5

theorem FUST.SpectralCoefficients.phi_sub_psi_eq_sqrt5_fib (n : ℕ) : φ ^ n - ψ ^ n = √5 * ↑(Nat.fib n)

φ^n - ψ^n = √5 · F_n

theorem FUST.SpectralCoefficients.Diff6Coeff_fib_spectralWeight (n : ℕ) : Diff6Coeff n = √5 * ↑(Nat.fib n) * spectralWeight n

Diff6Coeff via Fibonacci and spectral weight: C_n = √5 · F_n · Q_n

theorem FUST.SpectralCoefficients.fib_strong_divisibility (m n : ℕ) : Nat.fib (m.gcd n) = (Nat.fib m).gcd (Nat.fib n)

Strong divisibility: gcd(F_m, F_n) = F_{gcd(m,n)}

theorem FUST.SpectralCoefficients.fib_dvd_of_dvd (m n : ℕ) (h : m ∣ n) : Nat.fib m ∣ Nat.fib n

Divisor transfer: m | n → F_m | F_n

theorem FUST.SpectralCoefficients.fib_dvd_periodic (p k n : ℕ) (hk : p ∣ Nat.fib k) : p ∣ Nat.fib (n * k)

If p | F_k then p | F_{nk} for all n. Every prime reappears periodically.

theorem FUST.SpectralCoefficients.rank_apparition_2 : 2 ∣ Nat.fib 3

Concrete ranks of apparition: α(2)=3

theorem FUST.SpectralCoefficients.rank_apparition_3 : 3 ∣ Nat.fib 4

α(3) = 4

theorem FUST.SpectralCoefficients.rank_apparition_5 : 5 ∣ Nat.fib 5

α(5) = 5 (ramified prime, disc(ℚ(√5)) = 5)

theorem FUST.SpectralCoefficients.rank_apparition_7 : 7 ∣ Nat.fib 8

α(7) = 8

theorem FUST.SpectralCoefficients.rank_apparition_11 : 11 ∣ Nat.fib 10

α(11) = 10, (5/11) = 1 since 11 ≡ 1 (mod 5), and 10 | 11-1 = 10

theorem FUST.SpectralCoefficients.rank_apparition_13 : 13 ∣ Nat.fib 7

α(13) = 7, (5/13) = -1 since 13 ≡ 3 (mod 5), and 7 | 13+1 = 14

theorem FUST.SpectralCoefficients.rank_apparition_17 : 17 ∣ Nat.fib 9

α(17) = 9, (5/17) = -1 since 17 ≡ 2 (mod 5), and 9 | 17+1 = 18

theorem FUST.SpectralCoefficients.rank_apparition_29 : 29 ∣ Nat.fib 14

α(29) = 14, (5/29) = 1 since 29 ≡ 4 (mod 5), and 14 | 29-1 = 28

theorem FUST.SpectralCoefficients.rank_apparition_89 : 89 ∣ Nat.fib 11

α(89) = 11, (5/89) = 1 since 89 ≡ 4 (mod 5), and 11 | 89-1 = 88

theorem FUST.SpectralCoefficients.Diff6Coeff_zero_iff_fib_or_weight (n : ℕ) : Diff6Coeff n = 0 ↔ Nat.fib n = 0 ∨ spectralWeight n = 0

Diff6Coeff is proportional to Fibonacci with spectral weight as coefficient. For n ≥ 3, the spectral weight is nonzero, so F_n = 0 ⟺ C_n = 0.

theorem FUST.SpectralCoefficients.Diff6_prime_encoding_summary : (∀ (n : ℕ), Diff6Coeff n = √5 * ↑(Nat.fib n) * spectralWeight n) ∧ (∀ (m n : ℕ), Nat.fib (m.gcd n) = (Nat.fib m).gcd (Nat.fib n)) ∧ 2 ∣ Nat.fib 3 ∧ 3 ∣ Nat.fib 4 ∧ 5 ∣ Nat.fib 5 ∧ 7 ∣ Nat.fib 8 ∧ 11 ∣ Nat.fib 10 ∧ 13 ∣ Nat.fib 7 ∧ 29 ∣ Nat.fib 14 ∧ 89 ∣ Nat.fib 11

Summary: Diff6 spectral coefficients encode all primes via Fibonacci.

The chain: Diff6 → C_n = √5·F_n·Q_n → F_n (Fibonacci) → p | F_{α(p)} Every prime p enters the Fibonacci sequence at rank α(p) ≤ p+1. By strong divisibility gcd(F_m,F_n) = F_{gcd(m,n)}, the prime p divides F_n for exactly those n that are multiples of α(p).

The Frobenius element Frob_p ∈ Gal(ℚ(√5)/ℚ) determines α(p): (5/p) = 1 (p splits in ℤ[φ]): α(p) | p-1 (5/p) = -1 (p inert in ℤ[φ]): α(p) | p+1 p = 5 (ramified): α(5) = 5

This connects Diff6 (living in ℚ(√5)) to ζ(s) through: ζ_{ℚ(√5)}(s) = ζ(s) · L(s, χ_5)

Section 2.8: Dedekind Zeta Factorization for ℚ(√5)

The Dedekind zeta function of ℚ(√5) factors as ζ_{ℚ(√5)}(s) = ζ(s)·L(s,χ₅) where χ₅ is the Kronecker character mod 5. We prove the local Euler factor identity at each prime, which is the algebraic core of this factorization.

The splitting type of p in ℤ[φ] = ℤ[(1+√5)/2] determines the local factor: split (χ₅(p)=1): (1-p⁻ˢ)⁻² — p splits into two principal ideals inert (χ₅(p)=-1): (1-p⁻²ˢ)⁻¹ — p remains prime in ℤ[φ] ramified (χ₅(p)=0): (1-p⁻ˢ)⁻¹ — p=5 ramifies (disc(ℚ(√5))=5)

def FUST.SpectralCoefficients.chi5Fun (n : ℕ) : ℤ

Kronecker character χ₅ defined by values mod 5: χ₅(n) = (5|n).

Equations

• FUST.SpectralCoefficients.chi5Fun n = match n % 5 with | 0 => 0 | 1 => 1 | 2 => -1 | 3 => -1 | 4 => 1 | x => 0

theorem FUST.SpectralCoefficients.chi5Fun_zero : chi5Fun 0 = 0

theorem FUST.SpectralCoefficients.chi5Fun_one : chi5Fun 1 = 1

theorem FUST.SpectralCoefficients.chi5Fun_two : chi5Fun 2 = -1

theorem FUST.SpectralCoefficients.chi5Fun_three : chi5Fun 3 = -1

theorem FUST.SpectralCoefficients.chi5Fun_four : chi5Fun 4 = 1

theorem FUST.SpectralCoefficients.chi5Fun_five : chi5Fun 5 = 0

theorem FUST.SpectralCoefficients.chi5Fun_periodic (n : ℕ) : chi5Fun (n + 5) = chi5Fun n

theorem FUST.SpectralCoefficients.chi5Fun_values (n : ℕ) : chi5Fun n = 0 ∨ chi5Fun n = 1 ∨ chi5Fun n = -1

theorem FUST.SpectralCoefficients.chi5_split_11 : chi5Fun 11 = 1

theorem FUST.SpectralCoefficients.chi5_split_19 : chi5Fun 19 = 1

theorem FUST.SpectralCoefficients.chi5_split_29 : chi5Fun 29 = 1

theorem FUST.SpectralCoefficients.chi5_split_31 : chi5Fun 31 = 1

theorem FUST.SpectralCoefficients.chi5_split_41 : chi5Fun 41 = 1

theorem FUST.SpectralCoefficients.chi5_inert_2 : chi5Fun 2 = -1

theorem FUST.SpectralCoefficients.chi5_inert_3 : chi5Fun 3 = -1

theorem FUST.SpectralCoefficients.chi5_inert_7 : chi5Fun 7 = -1

theorem FUST.SpectralCoefficients.chi5_inert_13 : chi5Fun 13 = -1

theorem FUST.SpectralCoefficients.chi5_inert_17 : chi5Fun 17 = -1

theorem FUST.SpectralCoefficients.chi5_ramified_5 : chi5Fun 5 = 0

theorem FUST.SpectralCoefficients.euler_factor_chi_one (x : ℂ) : (1 - x)⁻¹ * (1 - 1 * x)⁻¹ = ((1 - x) ^ 2)⁻¹

Split factor: (1-x)⁻¹·(1-x)⁻¹ = ((1-x)²)⁻¹

theorem FUST.SpectralCoefficients.euler_factor_chi_neg_one (x : ℂ) : (1 - x)⁻¹ * (1 - -1 * x)⁻¹ = (1 - x ^ 2)⁻¹

Inert factor: (1-x)⁻¹·(1+x)⁻¹ = (1-x²)⁻¹

theorem FUST.SpectralCoefficients.euler_factor_chi_zero (x : ℂ) : (1 - x)⁻¹ * (1 - 0 * x)⁻¹ = (1 - x)⁻¹

Ramified factor: (1-x)⁻¹·1 = (1-x)⁻¹

theorem FUST.SpectralCoefficients.splitting_rank_apparition_consistency : (chi5Fun 11 = 1 ∧ 11 ∣ Nat.fib 10) ∧ (chi5Fun 29 = 1 ∧ 29 ∣ Nat.fib 14) ∧ (chi5Fun 31 = 1 ∧ 31 ∣ Nat.fib 30) ∧ (chi5Fun 2 = -1 ∧ 2 ∣ Nat.fib 3) ∧ (chi5Fun 3 = -1 ∧ 3 ∣ Nat.fib 4) ∧ (chi5Fun 7 = -1 ∧ 7 ∣ Nat.fib 8) ∧ (chi5Fun 13 = -1 ∧ 13 ∣ Nat.fib 7) ∧ chi5Fun 5 = 0 ∧ 5 ∣ Nat.fib 5

Connection: Fibonacci rank of apparition determines splitting type.

α(p) | p-1 ⟺ χ₅(p)=1 (split), α(p) | p+1 ⟺ χ₅(p)=-1 (inert). The Frobenius element Frob_p ∈ Gal(ℚ(√5)/ℚ) determines both α(p) and χ₅(p).

Section 3: Extended Diff₆ Kernel (ℤ → ℝ)

noncomputable def FUST.SpectralCoefficients.Diff6CoeffZ (n : ℤ) : ℝ

Equations

• FUST.SpectralCoefficients.Diff6CoeffZ n = FUST.φ ^ (3 * n) - 3 * FUST.φ ^ (2 * n) + FUST.φ ^ n - FUST.ψ ^ n + 3 * FUST.ψ ^ (2 * n) - FUST.ψ ^ (3 * n)

theorem FUST.SpectralCoefficients.Diff6CoeffZ_natCast (n : ℕ) : Diff6CoeffZ ↑n = Diff6Coeff n

theorem FUST.SpectralCoefficients.Diff6CoeffZ_zero : Diff6CoeffZ 0 = 0

theorem FUST.SpectralCoefficients.Diff6CoeffZ_one : Diff6CoeffZ 1 = 0

theorem FUST.SpectralCoefficients.Diff6CoeffZ_two : Diff6CoeffZ 2 = 0

theorem FUST.SpectralCoefficients.Diff6CoeffZ_neg_even (n : ℤ) (hn : Even n) : Diff6CoeffZ (-n) = -Diff6CoeffZ n

theorem FUST.SpectralCoefficients.Diff6CoeffZ_neg_two : Diff6CoeffZ (-2) = 0

theorem FUST.SpectralCoefficients.Diff6_extended_kernel_dim : Diff6CoeffZ (-2) = 0 ∧ Diff6CoeffZ 0 = 0 ∧ Diff6CoeffZ 1 = 0 ∧ Diff6CoeffZ 2 = 0

theorem FUST.SpectralCoefficients.Diff6CoeffZ_neg_one_ne_zero : Diff6CoeffZ (-1) ≠ 0

theorem FUST.SpectralCoefficients.Diff6CoeffZ_three_ne_zero : Diff6CoeffZ 3 ≠ 0

theorem FUST.SpectralCoefficients.Diff6CoeffZ_neg_three_ne_zero : Diff6CoeffZ (-3) ≠ 0

theorem FUST.SpectralCoefficients.Diff6_kernel_gap_structure : Diff6CoeffZ (-3) ≠ 0 ∧ Diff6CoeffZ (-2) = 0 ∧ Diff6CoeffZ (-1) ≠ 0 ∧ Diff6CoeffZ 0 = 0 ∧ Diff6CoeffZ 1 = 0 ∧ Diff6CoeffZ 2 = 0 ∧ Diff6CoeffZ 3 ≠ 0

Section 4: Diff₅ Spectral Coefficients

Diff₅(xⁿ) = Diff5Coeff(n) · x^{n-1} where Diff5Coeff(n) = φ^{2n} + φ^n + ψ^n + ψ^{2n} - 4 = L(2n) + L(n) - 4. ker(Diff₅) = {n | Diff5Coeff(n) = 0} = {0, 1} (polynomial), {0, 1} (Laurent).

noncomputable def FUST.SpectralCoefficients.Diff5CoeffZ (n : ℤ) : ℝ

Diff₅ spectral coefficient: Diff5Coeff(n) = φ^{2n} + φ^n + ψ^n + ψ^{2n} - 4

Equations

• FUST.SpectralCoefficients.Diff5CoeffZ n = FUST.φ ^ (2 * n) + FUST.φ ^ n + FUST.ψ ^ n + FUST.ψ ^ (2 * n) - 4

theorem FUST.SpectralCoefficients.Diff5CoeffZ_zero : Diff5CoeffZ 0 = 0

theorem FUST.SpectralCoefficients.Diff5CoeffZ_one : Diff5CoeffZ 1 = 0

theorem FUST.SpectralCoefficients.Diff5CoeffZ_two : Diff5CoeffZ 2 = 6

theorem FUST.SpectralCoefficients.Diff5CoeffZ_two_ne_zero : Diff5CoeffZ 2 ≠ 0

theorem FUST.SpectralCoefficients.Diff5CoeffZ_neg_two : Diff5CoeffZ (-2) = 6

theorem FUST.SpectralCoefficients.Diff5_kernel_structure : Diff5CoeffZ 0 = 0 ∧ Diff5CoeffZ 1 = 0 ∧ Diff5CoeffZ 2 ≠ 0 ∧ Diff5CoeffZ (-1) ≠ 0 ∧ Diff5CoeffZ (-2) ≠ 0

Diff₅ Laurent kernel: ker = {0, 1}, same as polynomial kernel

theorem FUST.SpectralCoefficients.Diff5Diff6_coeff_comparison_at_2 : Diff5CoeffZ 2 = 6 ∧ Diff6CoeffZ 2 = 0

Diff₅ and Diff₆ coefficients agree at d=2: both give 6 (Diff₅ detects, Diff₆ annihilates)