Rescaled symmetric operator: 5·Φ_S with ℤ[φ] coefficients

noncomputable def FUST.FζOperator.Φ_S_int (f : ℂ → ℂ) (z : ℂ) : ℂ

5·Φ_S: coefficients [10, 21-2φ, -50, 9+2φ, 10] ∈ ℤ[φ]

Equations

• FUST.FζOperator.Φ_S_int f z = 10 * f (↑FUST.φ ^ 2 * z) + (21 - 2 * ↑FUST.φ) * f (↑FUST.φ * z) - 50 * f z + (9 + 2 * ↑FUST.φ) * f (↑FUST.ψ * z) + 10 * f (↑FUST.ψ ^ 2 * z)

theorem FUST.FζOperator.Φ_S_int_eq (f : ℂ → ℂ) (z : ℂ) : Φ_S_int f z = 5 * DζOperator.Φ_S f z

Φ_S_int = 5 · Φ_S

Integral Dζ: Fζ = AFNum(5·Φ_A) + SymNum(Φ_S_int) = 5z·Dζ

noncomputable def FUST.FζOperator.Fζ (f : ℂ → ℂ) (z : ℂ) : ℂ

Fζ: integral form, closed on ℤ[φ,ζ₆][z]

Equations

• FUST.FζOperator.Fζ f z = FUST.DζOperator.AFNum (fun (w : ℂ) => 5 * FUST.DζOperator.Φ_A f w) z + FUST.DζOperator.SymNum (FUST.FζOperator.Φ_S_int f) z

theorem FUST.FζOperator.AFNum_smul (g : ℂ → ℂ) (c z : ℂ) : DζOperator.AFNum (fun (w : ℂ) => c * g w) z = c * DζOperator.AFNum g z

AFNum is linear: AFNum(c·g) = c · AFNum(g)

theorem FUST.FζOperator.SymNum_smul (g : ℂ → ℂ) (c z : ℂ) : DζOperator.SymNum (fun (w : ℂ) => c * g w) z = c * DζOperator.SymNum g z

SymNum is linear: SymNum(c·g) = c · SymNum(g)

theorem FUST.FζOperator.SymNum_of_Φ_S_int (f : ℂ → ℂ) (z : ℂ) : DζOperator.SymNum (Φ_S_int f) z = 5 * DζOperator.SymNum (DζOperator.Φ_S f) z

SymNum of rescaled: SymNum(5·g) = 5 · SymNum(g)

theorem FUST.FζOperator.Fζ_eq (f : ℂ → ℂ) (z : ℂ) (hz : z ≠ 0) : Fζ f z = 5 * z * DζOperator.Dζ f z

Fζ = 5z · Dζ

Kernel: Fζ annihilates {1, z²} (but NOT z: Dζ(id) ≠ 0)

theorem FUST.FζOperator.Fζ_kernel_const (z : ℂ) : Fζ (fun (x : ℂ) => 1) z = 0

theorem FUST.FζOperator.Fζ_kernel_quad (z : ℂ) : Fζ (fun (w : ℂ) => w ^ 2) z = 0

Fζ annihilates w² (ζ₆ squared-power cancellation in both channels)

Extended kernel: Fζ annihilates w³ and w⁴ (mod 6 vanishing)

Fζ(wⁿ) = 0 for all n with gcd(n,6) > 1. Both AFNum and SymNum kill w^n when n ≡ 0,2,3,4 mod 6 via ζ₆ root-of-unity cancellation.

theorem FUST.FζOperator.Fζ_kernel_cube (z : ℂ) : Fζ (fun (w : ℂ) => w ^ 3) z = 0

Fζ annihilates w³ (ζ₆³ = -1 cancellation in both channels)

theorem FUST.FζOperator.Fζ_kernel_fourth (z : ℂ) : Fζ (fun (w : ℂ) => w ^ 4) z = 0

Fζ annihilates w⁴ (ζ₆⁴ = -ζ₆ cancellation in both channels)

Translation equivariance: Fζ(f(c·))(z) = Fζ(f)(cz)

theorem FUST.FζOperator.Fζ_translate (f : ℂ → ℂ) (c z : ℂ) : Fζ (fun (t : ℂ) => f (c * t)) z = Fζ f (c * z)

General monomial factoring: Φ_A(wⁿ) and Φ_S_int(wⁿ)

theorem FUST.FζOperator.phiA_monomial (n : ℕ) (w : ℂ) : DζOperator.Φ_A (fun (t : ℂ) => t ^ n) w = (↑φ ^ (3 * n) - 4 * ↑φ ^ (2 * n) + (3 + ↑φ) * ↑φ ^ n - (3 + ↑ψ) * ↑ψ ^ n + 4 * ↑ψ ^ (2 * n) - ↑ψ ^ (3 * n)) * w ^ n

Φ_A factors on monomials: Φ_A(wⁿ)(z) = c_A(n) · zⁿ

theorem FUST.FζOperator.phiS_int_monomial (n : ℕ) (w : ℂ) : Φ_S_int (fun (t : ℂ) => t ^ n) w = (10 * ↑φ ^ (2 * n) + (21 - 2 * ↑φ) * ↑φ ^ n - 50 + (9 + 2 * ↑φ) * ↑ψ ^ n + 10 * ↑ψ ^ (2 * n)) * w ^ n

Φ_S_int factors on monomials: Φ_S_int(wⁿ)(z) = c_S(n) · zⁿ

Eigenvalue formula for n ≡ 1 mod 6

Fζ(w^{6k+1})(z) = (5·c_A·AF_coeff + 6·c_S) · z^{6k+1}

theorem FUST.FζOperator.Fζ_eigenvalue_mod6_1 (k : ℕ) (z : ℂ) : Fζ (fun (w : ℂ) => w ^ (6 * k + 1)) z = (5 * (↑φ ^ (3 * (6 * k + 1)) - 4 * ↑φ ^ (2 * (6 * k + 1)) + (3 + ↑φ) * ↑φ ^ (6 * k + 1) - (3 + ↑ψ) * ↑ψ ^ (6 * k + 1) + 4 * ↑ψ ^ (2 * (6 * k + 1)) - ↑ψ ^ (3 * (6 * k + 1))) * DζOperator.AF_coeff + 6 * (10 * ↑φ ^ (2 * (6 * k + 1)) + (21 - 2 * ↑φ) * ↑φ ^ (6 * k + 1) - 50 + (9 + 2 * ↑φ) * ↑ψ ^ (6 * k + 1) + 10 * ↑ψ ^ (2 * (6 * k + 1)))) * z ^ (6 * k + 1)

Fζ on w^{6k+1}: explicit eigenvalue formula

theorem FUST.FζOperator.Fζ_eigenvalue_mod6_5 (k : ℕ) (z : ℂ) : Fζ (fun (w : ℂ) => w ^ (6 * k + 5)) z = (-5 * (↑φ ^ (3 * (6 * k + 5)) - 4 * ↑φ ^ (2 * (6 * k + 5)) + (3 + ↑φ) * ↑φ ^ (6 * k + 5) - (3 + ↑ψ) * ↑ψ ^ (6 * k + 5) + 4 * ↑ψ ^ (2 * (6 * k + 5)) - ↑ψ ^ (3 * (6 * k + 5))) * DζOperator.AF_coeff + 6 * (10 * ↑φ ^ (2 * (6 * k + 5)) + (21 - 2 * ↑φ) * ↑φ ^ (6 * k + 5) - 50 + (9 + 2 * ↑φ) * ↑ψ ^ (6 * k + 5) + 10 * ↑ψ ^ (2 * (6 * k + 5)))) * z ^ (6 * k + 5)

Fζ on w^{6k+5}: eigenvalue with negated AF_coeff

General mod 6 vanishing: Fζ(z^n) = 0 when gcd(n,6) > 1

theorem FUST.FζOperator.Fζ_vanish_mod6_0 (k : ℕ) (z : ℂ) : Fζ (fun (w : ℂ) => w ^ (6 * k)) z = 0

theorem FUST.FζOperator.Fζ_vanish_mod6_2 (k : ℕ) (z : ℂ) : Fζ (fun (w : ℂ) => w ^ (6 * k + 2)) z = 0

theorem FUST.FζOperator.Fζ_vanish_mod6_3 (k : ℕ) (z : ℂ) : Fζ (fun (w : ℂ) => w ^ (6 * k + 3)) z = 0

theorem FUST.FζOperator.Fζ_vanish_mod6_4 (k : ℕ) (z : ℂ) : Fζ (fun (w : ℂ) => w ^ (6 * k + 4)) z = 0

Derivation defect: Fζ(fg) - f·Fζ(g) - Fζ(f)·g

The derivation defect of any linear operator L is the unique bilinear form δ_L(f,g) = L(fg) - f·L(g) - L(f)·g. This is not an arbitrary definition: it is the standard obstruction to L being a derivation.

noncomputable def FUST.FζOperator.derivDefect (f g : ℂ → ℂ) (z : ℂ) : ℂ

Derivation defect of Fζ evaluated at z

Equations

• FUST.FζOperator.derivDefect f g z = FUST.FζOperator.Fζ (fun (w : ℂ) => f w * g w) z - f z * FUST.FζOperator.Fζ g z - FUST.FζOperator.Fζ f z * g z

theorem FUST.FζOperator.derivDefect_monomial (a b : ℕ) (z : ℂ) : derivDefect (fun (w : ℂ) => w ^ a) (fun (w : ℂ) => w ^ b) z = Fζ (fun (w : ℂ) => w ^ (a + b)) z - z ^ a * Fζ (fun (w : ℂ) => w ^ b) z - Fζ (fun (w : ℂ) => w ^ a) z * z ^ b

On monomials: δ(zᵃ,zᵇ) = Fζ(z^{a+b}) - zᵃ·Fζ(zᵇ) - Fζ(zᵃ)·zᵇ

Emergence: ker × ker → active

When gcd(a,6)>1 and gcd(b,6)>1 but gcd(a+b,6)=1, the defect equals the full eigenvalue: δ(zᵃ,zᵇ) = Fζ(z^{a+b}).

theorem FUST.FζOperator.emergence_3_4 (z : ℂ) : derivDefect (fun (w : ℂ) => w ^ 3) (fun (w : ℂ) => w ^ 4) z = Fζ (fun (w : ℂ) => w ^ 7) z

z³·z⁴ → z⁷: both in ker, product is active

Fζ is ℂ-linear in the function argument

theorem FUST.FζOperator.Fζ_const_smul (c : ℂ) (f : ℂ → ℂ) (z : ℂ) : Fζ (fun (w : ℂ) => c * f w) z = c * Fζ f z

Gauge invariance: δ(c·f, c⁻¹·g) = δ(f, g) for constant c ∈ ℂ×

This follows from Fζ's ℂ-linearity and c·c⁻¹ = 1.

theorem FUST.FζOperator.derivDefect_const_gauge (c : ℂ) (hc : c ≠ 0) (f g : ℂ → ℂ) (z : ℂ) : derivDefect (fun (w : ℂ) => c * f w) (fun (w : ℂ) => c⁻¹ * g w) z = derivDefect f g z

GEI decomposition of eigenvalue

The eigenvalue 5·c_A·AF_coeff + 6·c_S decomposes as a+bφ+cζ₆+dφζ₆. Using AF_coeff = 4ζ₆-2 and grouping: the AF channel contributes to ζ₆ components while the SY channel contributes to the φ components.

General emergence: δ(ker, ker) = Fζ at active sum

For ANY kernel pair whose sum is active, the derivation defect equals the full Fζ eigenvalue. The two emergence channels are:

• mod 3 + mod 4 → mod 1 (matter)
• mod 2 + mod 3 → mod 5 (antimatter)

theorem FUST.FζOperator.emergence_matter (j k : ℕ) (z : ℂ) : derivDefect (fun (w : ℂ) => w ^ (6 * j + 3)) (fun (w : ℂ) => w ^ (6 * k + 4)) z = Fζ (fun (w : ℂ) => w ^ (6 * j + 3 + (6 * k + 4))) z

General matter emergence: δ(z^{6j+3}, z^{6k+4}) = Fζ(z^{6(j+k)+7})

theorem FUST.FζOperator.emergence_antimatter (j k : ℕ) (z : ℂ) : derivDefect (fun (w : ℂ) => w ^ (6 * j + 2)) (fun (w : ℂ) => w ^ (6 * k + 3)) z = Fζ (fun (w : ℂ) => w ^ (6 * j + 2 + (6 * k + 3))) z

General antimatter emergence: δ(z^{6j+2}, z^{6k+3}) = Fζ(z^{6(j+k)+5})

theorem FUST.FζOperator.emergence_normSq_matter (j k : ℕ) (z : ℂ) : Complex.normSq (derivDefect (fun (w : ℂ) => w ^ (6 * j + 3)) (fun (w : ℂ) => w ^ (6 * k + 4)) z) = Complex.normSq (Fζ (fun (w : ℂ) => w ^ (6 * j + 3 + (6 * k + 4))) z)

Emergence norm identity: |δ(ker,ker)(z)|² = |Fζ(z^{a+b})(z)|² Combined with eigenvalue evaluation, this gives |δ|² = tauNormSq.

theorem FUST.FζOperator.emergence_normSq_antimatter (j k : ℕ) (z : ℂ) : Complex.normSq (derivDefect (fun (w : ℂ) => w ^ (6 * j + 2)) (fun (w : ℂ) => w ^ (6 * k + 3)) z) = Complex.normSq (Fζ (fun (w : ℂ) => w ^ (6 * j + 2 + (6 * k + 3))) z)

τ-symmetry: charge conjugation from AF_coeff² = -12

The Galois involution τ: ζ₆ → 1-ζ₆ sends AF_coeff → -AF_coeff. For eigenvalues λ = ε·5c_A·AF + 6c_S, τ flips the AF sign. The key algebraic fact AF² = -12 makes the τ-norm positive definite.

theorem FUST.FζOperator.AF_coeff_sq : DζOperator.AF_coeff ^ 2 = -12

AF_coeff² = -12: the key identity for τ-norm

theorem FUST.FζOperator.tau_trace (c_A c_S : ℂ) : c_A * DζOperator.AF_coeff + c_S + (-c_A * DζOperator.AF_coeff + c_S) = 2 * c_S

τ-trace: (c_A·AF + c_S) + (-c_A·AF + c_S) = 2c_S

theorem FUST.FζOperator.eigenvalue_tau_trace (c_A c_S : ℂ) : 5 * c_A * DζOperator.AF_coeff + 6 * c_S + (-5 * c_A * DζOperator.AF_coeff + 6 * c_S) = 12 * c_S

Eigenvalue τ-trace on Fζ: mod1 + mod5 eigenvalues cancel AF channel. For any c_A, c_S, the sum of (5c_A·AF + 6c_S) and (-5c_A·AF + 6c_S) = 12c_S.

theorem FUST.FζOperator.eigenvalue_tau_norm (c_A c_S : ℂ) : (5 * c_A * DζOperator.AF_coeff + 6 * c_S) * (-5 * c_A * DζOperator.AF_coeff + 6 * c_S) = 36 * c_S ^ 2 + 300 * c_A ^ 2

Eigenvalue τ-norm on Fζ: product uses AF²=-12. (5c_A·AF + 6c_S)·(-5c_A·AF + 6c_S) = 36c_S² + 300c_A².

Hermitian/anti-Hermitian structure of AFNum and SymNum

For any function g satisfying Schwarz reflection g(conj z) = conj(g z), AFNum is anti-Hermitian and SymNum is Hermitian under complex conjugation. This gives the algebraic origin of spacetime: AF = space, SY = time.

Key identities: ζ₆⁵ = ζ₆' = conj(ζ₆), ζ₆⁴ = conj(ζ₆²), ζ₆³ = -1.

theorem FUST.FζOperator.AFNum_anti_hermitian (g : ℂ → ℂ) (hg : ∀ (z : ℂ), g ((starRingEnd ℂ) z) = (starRingEnd ℂ) (g z)) (s : ℂ) : DζOperator.AFNum g ((starRingEnd ℂ) s) = -(starRingEnd ℂ) (DζOperator.AFNum g s)

AFNum is anti-Hermitian: AFNum(g)(s̄) = -conj(AFNum(g)(s)) when g satisfies Schwarz reflection g(z̄) = conj(g(z)).

theorem FUST.FζOperator.SymNum_hermitian (g : ℂ → ℂ) (hg : ∀ (z : ℂ), g ((starRingEnd ℂ) z) = (starRingEnd ℂ) (g z)) (s : ℂ) : DζOperator.SymNum g ((starRingEnd ℂ) s) = (starRingEnd ℂ) (DζOperator.SymNum g s)

SymNum is Hermitian: SymNum(g)(s̄) = conj(SymNum(g)(s)) when g satisfies Schwarz reflection g(z̄) = conj(g(z)).

theorem FUST.FζOperator.AFNum_real_pure_im (g : ℂ → ℂ) (hg : ∀ (z : ℂ), g ((starRingEnd ℂ) z) = (starRingEnd ℂ) (g z)) (s : ℝ) : (DζOperator.AFNum g ↑s).re = 0

For real s, AFNum is pure imaginary: Re(AFNum(g)(s)) = 0

theorem FUST.FζOperator.SymNum_real_pure_re (g : ℂ → ℂ) (hg : ∀ (z : ℂ), g ((starRingEnd ℂ) z) = (starRingEnd ℂ) (g z)) (s : ℝ) : (DζOperator.SymNum g ↑s).im = 0

For real s, SymNum is real: Im(SymNum(g)(s)) = 0

Spacetime √15 factorization: AF channel is pure imaginary, SY is real

theorem FUST.FζOperator.AF_channel_pure_im (A : ℝ) : (5 * ↑(√5 * A) * DζOperator.AF_coeff).re = 0

Re(5·(√5·A)·AF_coeff) = 0: AF channel is pure imaginary

theorem FUST.FζOperator.AF_channel_im (A : ℝ) : (5 * ↑(√5 * A) * DζOperator.AF_coeff).im = 10 * √15 * A

Im(5·(√5·A)·AF_coeff) = 10√15·A: space channel proportional to √15

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

Im(λ) = 10√15·A_n: eigenvalue space channel

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

Re(λ) = 6·c_S: eigenvalue time channel