Fζ Action on Scale Lattice

Sf = |Fζ f(φⁿ)|², partial sum over [-N, N].

noncomputable def FUST.actionFζ (f : ℂ → ℂ) (n : ℤ) : ℝ

Equations

• FUST.actionFζ f n = Complex.normSq (FUST.FζOperator.Fζ f ↑(FUST.φ ^ n))

theorem FUST.actionFζ_nonneg (f : ℂ → ℂ) (n : ℤ) : actionFζ f n ≥ 0

noncomputable def FUST.partialActionFζ (f : ℂ → ℂ) (N : ℕ) : ℝ

Equations

• FUST.partialActionFζ f N = ∑ n ∈ Finset.Icc (-↑N) ↑N, FUST.actionFζ f n

theorem FUST.partialActionFζ_nonneg (f : ℂ → ℂ) (N : ℕ) : partialActionFζ f N ≥ 0

theorem FUST.actionFζ_ker_zero (f : ℂ → ℂ) (hf : TimeStructure.IsInKerFζ f) (n : ℤ) : actionFζ f n = 0

theorem FUST.partialActionFζ_ker_zero (f : ℂ → ℂ) (hf : TimeStructure.IsInKerFζ f) (N : ℕ) : partialActionFζ f N = 0

theorem FUST.actionFζ_zero_iff (f : ℂ → ℂ) (n : ℤ) : actionFζ f n = 0 ↔ FζOperator.Fζ f ↑(φ ^ n) = 0

Mass Invariant from Dζ Eigenvalue

m²(s) = Dζ_im(s)² - Dζ_re(s)² = 12·Φ_A(s)² - 36·Φ_S(s)². Temporal component (AF channel, imaginary) minus spatial (SY channel, real). Minimum active mode s=1: m² = 144√5 - 84 = 12(12√5 - 7).

noncomputable def FUST.casimirMassSq (s : ℕ) : ℝ

Mass² from Dζ eigenvalue: Im² - Re² = 12·Φ_A² - 36·Φ_S²

Equations

• FUST.casimirMassSq s = FUST.Physics.Gravity.Dζ_im s ^ 2 - FUST.Physics.Gravity.Dζ_re s ^ 2

theorem FUST.casimirMassSq_def (s : ℕ) : casimirMassSq s = 12 * Physics.Gravity.Φ_A_coeff s ^ 2 - 36 * Physics.Gravity.Φ_S_coeff s ^ 2

theorem FUST.casimirMassSq_one : casimirMassSq 1 = 144 * √5 - 84

noncomputable def FUST.massGapSq : ℝ

Equations

• FUST.massGapSq = FUST.casimirMassSq 1

theorem FUST.massGapSq_eq : massGapSq = 144 * √5 - 84

theorem FUST.massGapSq_pos : 0 < massGapSq