Local-Gap Residual Layer

This file packages the residual contribution after the primary core region is removed.

The public theorems a reader should inspect first are:

• primaryCoreContribution
• residual_estimate_quantitative
• cubicT_sq_core_gaussian_correction_tail_le

The threshold bookkeeping lemmas immediately above residual_estimate_quantitative are implementation detail for that theorem.

def primaryCoreContribution (n t : ℕ) : ℝ

Equations

• primaryCoreContribution n t = Cn3Torus.texPrefactor n * ∫ (mu : Cn3Torus.Edge n → ℝ) in edgeCoreRegion n ↑t, (Cn3Torus.psi n mu ^ (4 * t)).re

theorem residual_estimate_quantitative : ∃ (c : ℝ) (K : ℝ) (C : ℝ), 0 < c ∧ 0 < K ∧ 0 < C ∧ ∀ (n : ℕ), 3 ≤ n → ∀ (t : ℕ), ↑t ≥ C * ↑n ^ 3 → |normalizedCount n (4 * t) - primaryCoreContribution n t| ≤ K * Real.exp (-(c * ↑n ^ 2)) * gaussianScale n ↑t

After discarding the primary core region, the remaining contribution is exponentially small in n² on the Gaussian scale at the n³ threshold.

theorem edgeCoreRegion_compl_gaussian_integral_le_exp_neg_dim_mul_gaussianF : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ) (t : ℝ), 1 ≤ t → ∫ (mu : Cn3Torus.Edge n → ℝ) in (edgeCoreRegion n t)ᶜ, Real.exp (-2 * t * Cn3Torus.sqNormEdge n mu) ≤ Real.exp (-(c * ↑(dim n))) * gaussianF (dim n) t

The Gaussian mass outside the dynamic core is exponentially small in the edge-space dimension. This is the complement form of coreMass_gap_le_exp_gaussianF.

theorem cubicT_sq_core_gaussian_correction_tail_le : ∃ (c : ℝ) (K : ℝ), 0 < c ∧ 0 < K ∧ ∀ (n : ℕ) (t : ℝ), 1 ≤ t → |(8 * t ^ 2 * ∫ (mu : Cn3Torus.Edge n → ℝ) in edgeCoreRegion n t, cubicT n (matrixOfEdge n mu) ^ 2 * Real.exp (-2 * t * Cn3Torus.sqNormEdge n mu)) - ↑(n.choose 3) / (8 * t) * gaussianF (dim n) t| ≤ K * (↑n ^ 3 / t) * Real.exp (-(c * ↑(dim n))) * gaussianF (dim n) t

Replacing the core-restricted cubic second moment by the exact full Gaussian moment costs only an exponentially small factor in the dimension.