noncomputable def Frourio.Qζ_disc [ZetaLineAPI] (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (Δτ Δξ : ℝ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ℝ

Discrete quadratic form specialized to the zeta kernel.

Equations

• Frourio.Qζ_disc w Δτ Δξ g = Frourio.Qdisc (fun (τ : ℝ) => Frourio.Kzeta τ) w Δτ Δξ g

noncomputable def Frourio.Δτφ (φ : ℝ) : ℝ

Golden lattice spacing Δτ = π / log φ.

Equations

• Frourio.Δτφ φ = zeroLatticeSpacing φ

noncomputable def Frourio.Δξφ (φ : ℝ) : ℝ

Dual lattice step choice, nominally Δξ = 2π / Δτ.

Equations

• Frourio.Δξφ φ = 2 * Real.pi / Frourio.Δτφ φ

noncomputable def Frourio.Qζ_discφ [ZetaLineAPI] (φ : ℝ) (w g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ℝ

Zeta discrete quadratic form on the golden lattice.

Equations

• Frourio.Qζ_discφ φ w g = Frourio.Qζ_disc w (Frourio.Δτφ φ) (Frourio.Δξφ φ) g

def Frourio.Qζ_bounds [ZetaLineAPI] (φ : ℝ) (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Prop

Two-sided bounds (design-level) for the zeta discrete quadratic form on the golden lattice.

Equations

• One or more equations did not get rendered due to their size.

def Frourio.Qζ_gamma [ZetaLineAPI] (φ : ℝ) (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Prop

Γ-convergence statement specialized to the zeta kernel with golden sampling.

Equations

• One or more equations did not get rendered due to their size.

structure Frourio.QζBoundsHypotheses [ZetaLineAPI] (φ : ℝ) (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Prop

Phase 2.3: Bounds hypotheses wrapper providing the existence of constants. This serves as a handoff point for the analytic proof that supplies explicit constants c1, c2 satisfying Qζ_bounds.

• exists_bounds : Qζ_bounds φ w

theorem Frourio.Qζ_bounds_proof [ZetaLineAPI] (φ : ℝ) (_hφ : 1 < φ) (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (h : QζBoundsHypotheses φ w) : Qζ_bounds φ w

Phase 2.3: From bounds hypotheses, conclude the two-sided control result.