Weak Invariance Input

This file isolates the weak invariance statement, in the sense of Mossel-O'Donnell-Oleszkiewicz, that is sufficient for the far-shell integral replacement.

It is kept separate so the comparison theorem and its influence hypotheses can be read independently of the later counting arguments.

theorem quadraticForm_lindeberg_comparison_C3 (N : ℕ) (f : Fin N → Fin N → ℝ) (hsymm : ∀ (i j : Fin N), f i j = f j i) (hdiag : ∀ (i : Fin N), f i i = 0) (φ : ℝ → ℝ) (M : ℝ) (hM_nonneg : 0 ≤ M) (hφ : ContDiff ℝ 3 φ) (hφ3 : ∀ (x : ℝ), |iteratedDeriv 3 φ x| ≤ M) : |(avgSigns N fun (σ : Fin N → Fin 2) => φ (Q2Signs N f σ)) - stdGaussianAvg N fun (x : Fin N → ℝ) => φ (Q2Gauss N f x)| ≤ 6 * M * ∑ k : Fin N, kernelInfluence N f k * √(kernelInfluence N f k)

Paper-facing C^3 Lindeberg comparison for degree-2 quadratic forms.

This compares the sign and Gaussian quadratic-form averages for a symmetric kernel with zero diagonal. The conclusion is the standard C^3 Lindeberg bound:

|E[φ(Q_f(X))) - E[φ(Q_f(G))]| ≤ 6 M * Σ Inf_k(f)^(3/2).

theorem psi_sub_gaussianPsi_le_threeHalfInfluenceSum (n : ℕ) (lam : Fin n → Fin n → ℝ) : ‖psi n lam - gaussianPsi n lam‖ ≤ 3 / 2 * threeHalfInfluenceSum n lam

Weak invariance bound in the project normalization.

This is the direct comparison theorem needed for the J-split far-shell argument. It bounds the gap between psi and gaussianPsi by (3 / 2) * threeHalfInfluenceSum n lam, where the latter encodes the sum of row influences raised to the 3/2 power.

theorem edgeEvenFarShell_contribution_bound_Jsplit (r : ℝ) (hr : 0 < r) (_hr' : r < Real.pi / 4) : ∃ (qSm : ℝ) (qBig : ℝ) (a : ℝ), 0 < qSm ∧ qSm < 1 ∧ 0 < qBig ∧ qBig < 1 ∧ 0 < a ∧ ∀ (n t : ℕ), 2 ≤ n → 1 ≤ t → Cn3Torus.texPrefactor n * ∫ (mu : Cn3Torus.Edge n → ℝ) in edgeEvenFarShell n r, ‖Cn3Torus.psi n mu‖ ^ (4 * t) ≤ qSm ^ (4 * t) + qBig ^ (4 * t) + Real.exp (-(a * ↑t / ↑n ^ (2 / 3)))

The direct far-shell integral bound proved from the J-split argument.

This is the theorem surface consumed by the local-gap file:

the weighted even far-shell contribution is bounded by three terms:

• qSm^(4t), a small-radius decay term
• qBig^(4t), a uniform box-decay term
• exp (-(a * t) / n^(2/3)), the MOO/invariance contribution