Local-Gap Bridge Layer

This file contains the shared local-gap support used by both the residual and fixed-n modules.

The first public theorems a reader should inspect are:

• gaussianScale_eq_texPrefactor_mul_gaussianF
• exactCore_correctedCore_gap_abs_le_gaussianF_short
• correctedCore_quarticCore_gap_abs_le_gaussianF_short
• quarticCore_cubicCore_gap_abs_le_gaussianF_short

Most other declarations here are implementation detail for those bridge statements or for downstream residual/fixed-n estimates.

theorem gaussianScale_eq_texPrefactor_mul_gaussianF (n : ℕ) (hn : 2 ≤ n) (t : ℝ) (ht : 0 < t) : Cn3Torus.texPrefactor n * gaussianF (dim n) t = gaussianScale n t

The Gaussian normalizer factors exactly as the tex prefactor times gaussianF.

theorem coreMass_le_gaussianF (n : ℕ) (t : ℝ) (ht : 0 < t) : coreMass (dim n) t ≤ gaussianF (dim n) t

The inner-core Gaussian mass is bounded above by the full Gaussian mass.

theorem one_le_dim_of_three_le (n : ℕ) (hn : 3 ≤ n) : 1 ≤ dim n

For n ≥ 3, the edge-space dimension is at least one.

theorem exp_neg_dim_over_eight_le_exp_neg_nsq_div_thirty_two {n : ℕ} (hn : 2 ≤ n) : Real.exp (-(↑(dim n) / 8)) ≤ Real.exp (-(↑n ^ 2 / 32))

The standard annulus factor exp(-dim/8) is at most exp(-n^2/32) once n ≥ 2.

theorem exp_neg_c_mul_dim_le_exp_neg_c_div_four_mul_nsq {n : ℕ} (hn : 2 ≤ n) {c : ℝ} (hc : 0 ≤ c) : Real.exp (-(c * ↑(dim n))) ≤ Real.exp (-(c / 4 * ↑n ^ 2))

A generic conversion from exponential decay in dim n to exponential decay in n², using dim n ≥ n² / 4.

theorem dim_div_t_le_inv_C (n t : ℕ) {C : ℝ} (hC_pos : 0 < C) (hC_one : 1 ≤ C) (hn_pos : 0 < n) (ht : ↑t ≥ C * ↑n ^ 3) : ↑(dim n) / ↑t ≤ 1 / C

At the t \ge C n^3 scale, dim / t is O(1/C).

theorem n_mul_sq_dim_div_t_le_inv_C (n t : ℕ) {C : ℝ} (hC_pos : 0 < C) (hC_one : 1 ≤ C) (hn_pos : 0 < n) (ht : ↑t ≥ C * ↑n ^ 3) : ↑n * (↑(dim n) / ↑t) ^ 2 ≤ 1 / C

At the t \ge C n^3 scale, the quartic n (dim/t)^2 parameter is O(1/C).

theorem n_cube_div_t_le_inv_C (n t : ℕ) {C : ℝ} (hC_pos : 0 < C) (hn_pos : 0 < n) (ht : ↑t ≥ C * ↑n ^ 3) : ↑n ^ 3 / ↑t ≤ 1 / C

At the t \ge C n^3 scale, the cubic bridge parameter n^3/t is O(1/C).

noncomputable def gaussianEvenMomentEnvelope (K : ℕ) : ℝ

A finite envelope for the even Gaussian moment coefficients up to degree 2K.

Equations

• gaussianEvenMomentEnvelope K = ∑ r ∈ Finset.range (K + 1), max 1 (gaussianEvenMomentCoeff✝ r)

theorem gaussianEvenMomentEnvelope_one_le (K : ℕ) : 1 ≤ gaussianEvenMomentEnvelope K

theorem quarticCorr_pointwise_bound_uniform : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ) (lam : Fin n → Fin n → ℝ), |quarticCorr n lam| ≤ C * sNorm n lam ^ 2

The quartic correction admits a uniform O(s^2) bound.

theorem cubicT_pointwise_bound_uniform : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ) (lam : Fin n → Fin n → ℝ), |cubicT n lam| ≤ C * sNorm n lam ^ (3 / 2)

Dimension-free cubic-form bound.

theorem psi_pow_sub_correctedCoreIntegrand_norm_le_uniform : ∃ (c₂ : ℝ) (C₂ : ℝ), 0 < c₂ ∧ 0 < C₂ ∧ ∀ (n t : ℕ) (mu : Cn3Torus.Edge n → ℝ), Cn3Torus.sqNormEdge n mu ≤ c₂ → 4 * ↑t * C₂ * Cn3Torus.sqNormEdge n mu ^ 3 ≤ 1 → ‖Cn3Torus.psi n mu ^ (4 * t) - correctedCoreIntegrand n t mu‖ ≤ 8 * ↑t * C₂ * Cn3Torus.sqNormEdge n mu ^ 3 * Real.exp (-2 * ↑t * Cn3Torus.sqNormEdge n mu + 4 * ↑t * quarticCorr n (matrixOfEdge n mu))

theorem cubicCoreIntegrand_re (n t : ℕ) (mu : Cn3Torus.Edge n → ℝ) : (cubicCoreIntegrand n t mu).re = Real.exp (-2 * ↑t * Cn3Torus.sqNormEdge n mu) * Real.cos (4 * ↑t * cubicT n (matrixOfEdge n mu))

The real part of the cubic core integrand is the Gaussian-cosine model from cubic_core_lower_bound.

theorem edgeEuclidBall_subset_edgeBox (n : ℕ) {r delta : ℝ} (hr_nonneg : 0 ≤ r) (hr : r ≤ delta) : edgeEuclidBall n r ⊆ edgeBox n delta

A Euclidean ball in edge coordinates sits inside the coordinate box of the same radius.

theorem cs_helper {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {f g : α → ℝ} (hf_ae : MeasureTheory.AEStronglyMeasurable f μ) (hg_ae : MeasureTheory.AEStronglyMeasurable g μ) (hf_nonneg : 0 ≤ᵐ[μ] f) (hg_nonneg : 0 ≤ᵐ[μ] g) (hf_int : MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ) (hg_int : MeasureTheory.Integrable (fun (x : α) => g x ^ 2) μ) : ∫ (x : α), f x * g x ∂μ ≤ (∫ (x : α), f x ^ 2 ∂μ) ^ (1 / 2) * (∫ (x : α), g x ^ 2 ∂μ) ^ (1 / 2)

Real Cauchy-Schwarz on an arbitrary measure space, specialized to the L² controls used in the four-bridge argument.

noncomputable def triangleTripleValidEquivFinsetCard3 (n : ℕ) : { τ : TriangleTriple✝ n // IsTriangleTriple✝ τ } ≃ { s : Finset (Fin n) // s.card = 3 }

Equations

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

theorem cubicT_sq_full_gaussian_correction_exact (n : ℕ) (t : ℝ) (ht : 0 < t) : 8 * t ^ 2 * ∫ (mu : Cn3Torus.Edge n → ℝ), cubicT n (matrixOfEdge n mu) ^ 2 * Real.exp (-2 * t * Cn3Torus.sqNormEdge n mu) = ↑(n.choose 3) / (8 * t) * gaussianF (dim n) t

instance instDecidableEqQuarticCycleShape : DecidableEq QuarticCycleShape✝

Equations

• instDecidableEqQuarticCycleShape x✝ y✝ = if h : QuarticCycleShape.ctorIdx✝ x✝ = QuarticCycleShape.ctorIdx✝¹ y✝ then isTrue ⋯ else isFalse ⋯

instance instFintypeQuarticCycleShape : Fintype QuarticCycleShape✝

Equations

• instFintypeQuarticCycleShape = { elems := { val := ↑QuarticCycleShape.enumList✝, nodup := QuarticCycleShape.enumList_nodup✝ }, complete := instFintypeQuarticCycleShape._proof_1 }

instance instDecidableEqTriangleEdgeShape : DecidableEq TriangleEdgeShape✝

Equations

• instDecidableEqTriangleEdgeShape x✝ y✝ = if h : TriangleEdgeShape.ctorIdx✝ x✝ = TriangleEdgeShape.ctorIdx✝¹ y✝ then isTrue ⋯ else isFalse ⋯

instance instFintypeTriangleEdgeShape : Fintype TriangleEdgeShape✝

Equations

• instFintypeTriangleEdgeShape = { elems := { val := ↑TriangleEdgeShape.enumList✝, nodup := TriangleEdgeShape.enumList_nodup✝ }, complete := instFintypeTriangleEdgeShape._proof_1 }

instance instDecidableEqQuinticEdgeTriangleLabel : DecidableEq QuinticEdgeTriangleLabel✝

Equations

• instDecidableEqQuinticEdgeTriangleLabel x✝ y✝ = if h : QuinticEdgeTriangleLabel.ctorIdx✝ x✝ = QuinticEdgeTriangleLabel.ctorIdx✝¹ y✝ then isTrue ⋯ else isFalse ⋯

instance instFintypeQuinticEdgeTriangleLabel : Fintype QuinticEdgeTriangleLabel✝

Equations

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

theorem cubicT_fourth_full_gaussian_integrable (n : ℕ) (t : ℝ) (ht : 0 < t) : MeasureTheory.Integrable (fun (mu : Cn3Torus.Edge n → ℝ) => cubicT n (matrixOfEdge n mu) ^ 4 * Real.exp (-2 * t * Cn3Torus.sqNormEdge n mu)) MeasureTheory.volume

theorem cubicT_fourth_full_gaussian_bound_explicit (n : ℕ) (t : ℝ) (ht : 1 ≤ t) : ∫ (mu : Cn3Torus.Edge n → ℝ), cubicT n (matrixOfEdge n mu) ^ 4 * Real.exp (-2 * t * Cn3Torus.sqNormEdge n mu) ≤ 7 * 6 ^ 12 * gaussianEvenMomentEnvelope 6 ^ 6 * ↑n ^ 6 / t ^ 6 * gaussianF (dim n) t

theorem cubic_core_second_order_gap_uniform : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ) (t : ℝ), 1 ≤ t → |(∫ (mu : Cn3Torus.Edge n → ℝ) in edgeCoreRegion n t, Real.exp (-2 * t * Cn3Torus.sqNormEdge n mu) * Real.cos (4 * t * cubicT n (matrixOfEdge n mu))) - (coreMass (dim n) 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))| ≤ C * ↑n ^ 6 / t ^ 2 * gaussianF (dim n) t

On the dynamic core, the cubic oscillatory factor admits the explicit second-order expansion with a fourth-moment remainder. This is the first quantitative theorem that uses the new T^4 machinery.

theorem correctedCoreIntegrand_sub_quarticCoreIntegrand_norm_le (n t : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ‖correctedCoreIntegrand n t mu - quarticCoreIntegrand n t mu‖ ≤ 4 * ↑t * |quinticP5 n (matrixOfEdge n mu)| * Real.exp (-2 * ↑t * Cn3Torus.sqNormEdge n mu + 4 * ↑t * quarticCorr n (matrixOfEdge n mu))

Removing the quintic phase costs only the size of the real quintic phase itself.

theorem small_ball_gaussian_decay_uniform : ∃ (r₀ : ℝ), 0 < r₀ ∧ r₀ < Real.pi / 4 ∧ ∀ (n : ℕ) (mu : Cn3Torus.Edge n → ℝ), Cn3Torus.sqNormEdge n mu ≤ r₀ ^ 2 → ∀ (t : ℕ), 1 ≤ t → ‖Cn3Torus.psi n mu‖ ^ (4 * t) ≤ Real.exp (-(3 * ↑t * Cn3Torus.sqNormEdge n mu / 2))

A uniform small-ball decay bound for the edge characteristic function.

theorem edgePrimaryLocalAnnulus_integral_bound_coreMass_uniform : ∃ (r₁ : ℝ) (C₆ : ℝ), 0 < r₁ ∧ 0 < C₆ ∧ r₁ < Real.pi / 4 ∧ ∀ (n : ℕ), 1 ≤ dim n → ∀ {r delta : ℝ}, 0 < r → r ≤ r₁ → ∀ (t : ℕ), 1 ≤ t → ∫ (mu : Cn3Torus.Edge n → ℝ) in (edgeBox n delta ∩ edgeEuclidBall n r) \ edgeCoreRegion n ↑t, ‖Cn3Torus.psi n mu‖ ^ (4 * t) ≤ C₆ * Real.exp (-(↑(dim n) / 8)) * coreMass (dim n) ↑t

The primary annulus contribution is uniformly exponentially small relative to coreMass.

theorem texPrefactor_nonneg (n : ℕ) : 0 ≤ Cn3Torus.texPrefactor n

The tex prefactor is always nonnegative.

theorem abs_integral_re_sub_le_integral_norm (n : ℕ) {s : Set (Cn3Torus.Edge n → ℝ)} {f g : (Cn3Torus.Edge n → ℝ) → ℂ} (hf : MeasureTheory.IntegrableOn f s MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g s MeasureTheory.volume) : |(∫ (x : Cn3Torus.Edge n → ℝ) in s, (f x).re) - ∫ (x : Cn3Torus.Edge n → ℝ) in s, (g x).re| ≤ ∫ (x : Cn3Torus.Edge n → ℝ) in s, ‖f x - g x‖

Real parts of complex set integrals are controlled by the integral of the complex norm difference.

theorem abs_integral_re_le_integral_norm (n : ℕ) {s : Set (Cn3Torus.Edge n → ℝ)} {f : (Cn3Torus.Edge n → ℝ) → ℂ} (hf : MeasureTheory.IntegrableOn f s MeasureTheory.volume) : |∫ (x : Cn3Torus.Edge n → ℝ) in s, (f x).re| ≤ ∫ (x : Cn3Torus.Edge n → ℝ) in s, ‖f x‖

Special case of abs_integral_re_sub_le_integral_norm against zero.

theorem exp_neg_mul_t_le_exp_neg_nsq_mul_gaussianScale_uniform_ge_three (a : ℝ) (ha : 0 < a) : ∃ (c : ℝ) (C : ℝ), 0 < c ∧ 0 < C ∧ ∀ (n : ℕ), 3 ≤ n → ∀ (t : ℕ), ↑t ≥ C * ↑n ^ 3 → Real.exp (-a * ↑t) ≤ Real.exp (-(c * ↑n ^ 2)) * gaussianScale n ↑t

A quantitative version of exp_neg_mul_t_le_eps_gaussianScale_uniform_ge_three with an explicit exp(-c n^2) factor on the Gaussian scale.

theorem qpow_le_exp_neg_nsq_mul_gaussianScale_uniform_ge_three (q : ℝ) (hq_pos : 0 < q) (hq_lt : q < 1) : ∃ (c : ℝ) (C : ℝ), 0 < c ∧ 0 < C ∧ ∀ (n : ℕ), 3 ≤ n → ∀ (t : ℕ), ↑t ≥ C * ↑n ^ 3 → q ^ (4 * t) ≤ Real.exp (-(c * ↑n ^ 2)) * gaussianScale n ↑t

A strict geometric decay on the far shell is bounded by an explicit exp(-c n^2) multiple of the Gaussian scale at the n^3 threshold.

theorem exp_neg_mul_t_div_n_two_thirds_le_exp_neg_nsq_mul_gaussianScale_uniform_ge_three (a : ℝ) (ha : 0 < a) : ∃ (c : ℝ) (C : ℝ), 0 < c ∧ 0 < C ∧ ∀ (n : ℕ), 3 ≤ n → ∀ (t : ℕ), ↑t ≥ C * ↑n ^ 3 → Real.exp (-(a * ↑t / ↑n ^ (2 / 3))) ≤ Real.exp (-(c * ↑n ^ 2)) * gaussianScale n ↑t

A quantitative version of exp_neg_mul_t_div_n_two_thirds_le_eps_gaussianScale_uniform_ge_three with an explicit exp(-c n^2) factor on the Gaussian scale.

theorem coreMass_gap_le_exp_gaussianF : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ) (t : ℝ), 1 ≤ t → |coreMass (dim n) t - gaussianF (dim n) t| ≤ Real.exp (-(c * ↑(dim n))) * gaussianF (dim n) t

The truncated Gaussian core differs from the full Gaussian mass by an exponentially small factor in the dimension.

theorem edgeBox_delta_subset_pi_div_four (n : ℕ) : edgeBox n Cn3Torus.delta ⊆ edgeBox n (Real.pi / 4)

theorem measurableSet_edgeEvenFarShell (n : ℕ) (r : ℝ) : MeasurableSet (edgeEvenFarShell n r)

The even far shell is measurable.

theorem continuous_correctedCoreIntegrand (n t : ℕ) : Continuous fun (mu : Cn3Torus.Edge n → ℝ) => correctedCoreIntegrand n t mu

Continuity of the repaired core integrand in edge coordinates.

theorem continuous_quarticCoreIntegrand (n t : ℕ) : Continuous fun (mu : Cn3Torus.Edge n → ℝ) => quarticCoreIntegrand n t mu

Continuity of the quartic core integrand in edge coordinates.

theorem continuous_cubicCoreIntegrand (n t : ℕ) : Continuous fun (mu : Cn3Torus.Edge n → ℝ) => cubicCoreIntegrand n t mu

Continuity of the cubic core integrand in edge coordinates.

theorem integralOn_mono_of_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} {f : α → ℝ} (hsubset : s ⊆ t) (hs : MeasurableSet s) (ht : MeasurableSet t) (hf_int : MeasureTheory.IntegrableOn f t μ) (hf_nonneg : 0 ≤ᵐ[μ.restrict t] f) : ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in t, f x ∂μ

Monotonicity of set integrals for nonnegative real functions.

theorem localIntegral_sub_core_abs_le_annulus_plus_far (n t : ℕ) (hbox : ↑(dim n) / ↑t ≤ Cn3Torus.delta ^ 2) (r : ℝ) : have box := edgeBox n Cn3Torus.delta; have core := edgeCoreRegion n ↑t; have A := (box ∩ edgeEuclidBall n r) \ core; have B := (box \ edgeEuclidBall n r) \ core; |Cn3Torus.localIntegral n t - ∫ (mu : Cn3Torus.Edge n → ℝ) in core, (Cn3Torus.psi n mu ^ (4 * t)).re| ≤ (∫ (mu : Cn3Torus.Edge n → ℝ) in A, ‖Cn3Torus.psi n mu‖ ^ (4 * t)) + ∫ (mu : Cn3Torus.Edge n → ℝ) in B, ‖Cn3Torus.psi n mu‖ ^ (4 * t)

Splitting the local box into the dynamic core plus the two shell pieces used in the final argument.

theorem exactCore_correctedCore_gap_abs_le_gaussianF_short : ∃ (c : ℝ) (K : ℝ), 0 < c ∧ 0 < K ∧ ∀ (n : ℕ), 3 ≤ n → ∀ (t : ℕ), 1 ≤ t → ↑(dim n) / ↑t ≤ c → ↑n ^ 6 / ↑t ^ 2 ≤ c → |(∫ (mu : Cn3Torus.Edge n → ℝ) in edgeCoreRegion n ↑t, (Cn3Torus.psi n mu ^ (4 * t)).re) - ∫ (mu : Cn3Torus.Edge n → ℝ) in edgeCoreRegion n ↑t, (correctedCoreIntegrand n t mu).re| ≤ K * (↑n ^ 6 / ↑t ^ 2) * gaussianF (dim n) ↑t

Public bridge 1: the exact core integral is close to the corrected core model on the Gaussian scale with n^6 / t^2 loss.

theorem correctedCore_quarticCore_gap_abs_le_gaussianF_short : ∃ (c : ℝ) (K : ℝ), 0 < c ∧ 0 < K ∧ ∀ (n : ℕ), 2 ≤ n → ∀ (t : ℕ), 1 ≤ t → ↑(dim n) / ↑t ≤ c → ↑n * (↑(dim n) / ↑t) ^ 2 ≤ c → |(∫ (mu : Cn3Torus.Edge n → ℝ) in edgeCoreRegion n ↑t, (correctedCoreIntegrand n t mu).re) - ∫ (mu : Cn3Torus.Edge n → ℝ) in edgeCoreRegion n ↑t, (quarticCoreIntegrand n t mu).re| ≤ K * (↑n ^ (5 / 2) / ↑t ^ (3 / 2)) * gaussianF (dim n) ↑t

Public bridge 2: the corrected-core to quartic-core bridge with the natural t^{-3/2} decay.

theorem quarticCore_cubicCore_gap_abs_le_gaussianF_short : ∃ (c : ℝ) (K : ℝ), 0 < c ∧ 0 < K ∧ ∀ (n t : ℕ), 1 ≤ t → ↑(dim n) / ↑t ≤ c → ↑n * (↑(dim n) / ↑t) ^ 2 ≤ c → |(∫ (mu : Cn3Torus.Edge n → ℝ) in edgeCoreRegion n ↑t, (quarticCoreIntegrand n t mu).re) - ∫ (mu : Cn3Torus.Edge n → ℝ) in edgeCoreRegion n ↑t, (cubicCoreIntegrand n t mu).re| ≤ K * (↑n ^ 2 / ↑t) * gaussianF (dim n) ↑t

Public bridge 3: stripping the quartic correction costs only n^2 / t on the Gaussian scale.

theorem abs_sub_le_sum_abs_sub_six (x₀ x₁ x₂ x₃ x₄ x₅ x₆ : ℝ) : |x₀ - x₆| ≤ |x₀ - x₁| + |x₁ - x₂| + |x₂ - x₃| + |x₃ - x₄| + |x₄ - x₅| + |x₅ - x₆|

A six-step telescoping chain for absolute differences.

theorem div_le_eps_six_of_scaled_bound {K C ε : ℝ} (hC : 0 < C) (hε : 0 < ε) (hscaled : 6 * K / ε ≤ C) : K / C ≤ ε / 6

Convert the bookkeeping constraint 6 K / ε ≤ C into the useful bound K / C ≤ ε / 6.