Quartic Fiber Reduction

This file isolates the quartic peeling argument used in the local-gap bridge.

The public theorems a reader should inspect are:

• gaussian_integral_with_perturbation_bound
• quarticCoreTrunc_bound
• quartic_exponential_core_bound

Most of the intermediate linear-algebra, matrix-factorization, and fiber transport lemmas are internal implementation detail and are kept private.

Local quartic compatibility layer.

These declarations were removed from the old monolithic foundational file during API slimming, but the quartic bridge still uses them internally. Keep them local here so that support code compiles without re-bloating the public Base API.

theorem gaussian_integral_with_perturbation_bound (n : ℕ) (β D t : ℝ) (hβ : 0 ≤ β) (ht : 0 < t) (hsmall : β * (D / t) ≤ 1 / 2) (B : Fin n → Fin n → ℝ) (hB : sNorm n B ≤ D / t) : ∫ (x : Fin n → ℝ), Real.exp (-(2 * t * ∑ i : Fin n, x i ^ 2) + β * t / 2 * ∑ i : Fin n, ∑ j : Fin n, quarticPeelMatrix✝ n B i j * x i * x j) ≤ Real.exp (β ^ 2 / 2 * (D / t) ^ 2) * (Real.pi / (2 * t)) ^ (↑n / 2)

Gaussian integral bound after inserting the quartic perturbation matrix.

This is the basic quadratic-form estimate used to control the peeled quartic core by a Gaussian main term with an explicit exponential correction.

def edgeCoreRegionD (n : ℕ) (D t : ℝ) : Set (Cn3Torus.Edge n → ℝ)

Equations

• edgeCoreRegionD n D t = {mu : Cn3Torus.Edge n → ℝ | Cn3Torus.sqNormEdge n mu ≤ D / t}

noncomputable def quarticCoreDensity (β t : ℝ) (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ℝ

Equations

• quarticCoreDensity β t n mu = Real.exp (β * t * quarticCorr n (matrixOfEdge n mu)) * Real.exp (-2 * t * Cn3Torus.sqNormEdge n mu)

noncomputable def quarticCoreTrunc (β D t : ℝ) (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ℝ

Equations

• quarticCoreTrunc β D t n mu = (edgeCoreRegionD n D t).indicator (quarticCoreDensity β t n) mu

noncomputable def peeledQuarticDensity (β t : ℝ) (n : ℕ) (p : (Cn3Torus.Edge n → ℝ) × (Fin n → ℝ)) : ℝ

Equations

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

noncomputable def peeledQuarticTrunc (β D t : ℝ) (n : ℕ) (p : (Cn3Torus.Edge n → ℝ) × (Fin n → ℝ)) : ℝ

Equations

• peeledQuarticTrunc β D t n p = (peeledCoreRegionD✝ n D t).indicator (peeledQuarticDensity β t n) p

theorem measurableSet_edgeCoreRegionD (n : ℕ) (D t : ℝ) : MeasurableSet (edgeCoreRegionD n D t)

theorem quarticCoreTrunc_bound (β D t : ℝ) (hβ : 0 ≤ β) (hD : 0 ≤ D) (ht : 0 < t) (hsmall : β * (D / t) ≤ 1 / 2) (n : ℕ) : MeasureTheory.Integrable (quarticCoreTrunc β D t n) MeasureTheory.volume ∧ ∫ (mu : Cn3Torus.Edge n → ℝ), quarticCoreTrunc β D t n mu ≤ Real.exp (β ^ 2 / 2 * ↑n * (D / t) ^ 2) * gaussianF (dim n) t

Integrability and global bound for the truncated quartic core density.

theorem quartic_exponential_core_bound (β : ℝ) (hβ : 0 < β) : ∃ (c₁ : ℝ) (C₁ : ℝ), 0 < c₁ ∧ 0 < C₁ ∧ ∀ (n : ℕ) (t : ℝ), 0 < t → ↑(dim n) / t ≤ c₁ → ↑n * ↑(dim n) ^ 2 / t ^ 2 ≤ c₁ → ∫ (mu : Cn3Torus.Edge n → ℝ) in edgeCoreRegion n t, Real.exp (β * t * quarticCorr n (matrixOfEdge n mu)) * Real.exp (-2 * t * Cn3Torus.sqNormEdge n mu) ≤ C₁ * coreMass (dim n) t

Uniform quartic-core bound on the geometric edge core region.

This upgrades quarticCoreTrunc_bound from the peeled Gaussian model to the actual edge-core integral used in the local-gap bridge.