Residual Analytic Support For The Cn^3 Formalization

This module contains the triangle/quartic/cubic support estimates that feed the local-gap residual analysis. It is the last foundational layer before the higher-level bridge and residual modules.

Triangle Expansion

theorem triangle_formula (n : ℕ) (lam : Fin n → Fin n → ℝ) : cubicT n lam = ∑ i : Fin n, ∑ j : Fin n, ∑ k : Fin n, if i < j ∧ j < k then lam i j * lam i k * lam j k else 0

Expands the cubic statistic as an explicit sum over ordered triangles.

theorem pair_triangleThroughPair_eq_simpleCycle4LastCross (n : ℕ) (B : Fin n → Fin n → ℝ) (x : Fin n → ℝ) : (∑ i : Fin n, ∑ j : Fin n, if i < j then x i * x j * triangleThroughPair n B i j else 0) = simpleCycle4LastCross n B x

theorem fourth_cumulant_identity (n : ℕ) (lam : Fin n → Fin n → ℝ) : (momentX n lam 4 - 3 * sNorm n lam ^ 2) / 24 = quarticCorr n lam

Fourth cumulant identity: κ₄/24 = Q₄^corr(λ). The fourth cumulant κ₄ = μ₄ - 3μ₂² = μ₄ - 3s², and κ₄/24 = (μ₄ - 3s²)/24 = Q₄^corr.

Fourth-Moment and Gaussian Bounds

theorem complex_re_abs_le_norm (z : ℂ) : |z.re| ≤ ‖z‖

theorem complex_im_abs_le_norm (z : ℂ) : |z.im| ≤ ‖z‖

theorem complex_log_approx_quadratic (z : ℂ) (hz : ‖z‖ ≤ 1 / 2) : ‖Complex.log (1 + z) - z + z ^ 2 / 2‖ ≤ ‖z‖ ^ 3

theorem inner_core_gaussian_mass : ∃ (c_star : ℝ), 0 < c_star ∧ ∀ (d : ℕ) (t : ℝ), 1 ≤ t → coreMass d t ≥ (1 - Real.exp (-(c_star * ↑d))) * gaussianF d t

theorem gaussianF_le_const_mul_coreMass : ∃ (C : ℝ), 0 < C ∧ ∀ (d : ℕ) (t : ℝ), 1 ≤ d → 1 ≤ t → gaussianF d t ≤ C * coreMass d t

The Gaussian reference mass is controlled by a fixed multiple of coreMass.

Far-Shell and Off-Core Estimates

theorem edgeEvenFarShell_subset_edgeBox (n : ℕ) (r : ℝ) : edgeEvenFarShell n r ⊆ edgeBox n (Real.pi / 4)

theorem gaussian_integrable_edge (n : ℕ) (a : ℝ) (ha : 0 < a) : MeasureTheory.Integrable (fun (mu : Cn3Torus.Edge n → ℝ) => Real.exp (-a * Cn3Torus.sqNormEdge n mu)) MeasureTheory.volume

The ambient Gaussian kernel on edge coordinates is integrable.

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

Polynomial-Gaussian kernels on edge coordinates are integrable.

theorem texPrefactor_mul_edgeBox_pi_div_four_volume_le_one (n : ℕ) (hn : 2 ≤ n) : Cn3Torus.texPrefactor n * (MeasureTheory.volume (edgeBox n (Real.pi / 4))).toReal ≤ 1

theorem cos_two_mul_le_exp_neg_eight_div_pi_sq_sq {x : ℝ} (hx : |x| ≤ Real.pi / 4) : Real.cos (2 * x) ≤ Real.exp (-(8 / Real.pi ^ 2) * x ^ 2)

theorem avg_one_exp_neg_eight_div_pi_sq_le_exp_neg_two_div_pi_sq {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ 1) : (1 + Real.exp (-(8 / Real.pi ^ 2) * u)) / 2 ≤ Real.exp (-(2 / Real.pi ^ 2) * u)

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

The cubic-core L² kernel is globally integrable against the Gaussian weight.

def correctedCoreExponent (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ℂ

The corrected logarithmic core exponent, written in edge coordinates.

Equations

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

def correctedCoreIntegrand (n t : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ℂ

The repaired step-1 core model with quartic and quintic phases included.

Equations

• correctedCoreIntegrand n t mu = Complex.exp (↑(4 * t) * correctedCoreExponent n mu)

theorem correctedCoreExponent_re (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : (correctedCoreExponent n mu).re = -(Cn3Torus.sqNormEdge n mu / 2) + quarticCorr n (matrixOfEdge n mu)

theorem correctedCoreIntegrand_norm (n t : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ‖correctedCoreIntegrand n t mu‖ = Real.exp (-2 * ↑t * Cn3Torus.sqNormEdge n mu + 4 * ↑t * quarticCorr n (matrixOfEdge n mu))

def quarticCoreExponent (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ℂ

The intermediate core exponent that keeps the quartic term but drops the quintic phase.

Equations

• quarticCoreExponent n mu = ↑(-(Cn3Torus.sqNormEdge n mu / 2)) - Complex.I * ↑(cubicT n (matrixOfEdge n mu)) + ↑(quarticCorr n (matrixOfEdge n mu))

def quarticCoreIntegrand (n t : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ℂ

The quartic core model used between the repaired and cubic cores.

Equations

• quarticCoreIntegrand n t mu = Complex.exp (↑(4 * t) * quarticCoreExponent n mu)

def cubicCoreExponent (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ℂ

The pure cubic-Gaussian core exponent.

Equations

• cubicCoreExponent n mu = ↑(-(Cn3Torus.sqNormEdge n mu / 2)) - Complex.I * ↑(cubicT n (matrixOfEdge n mu))

def cubicCoreIntegrand (n t : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ℂ

The cubic-Gaussian core model.

Equations

• cubicCoreIntegrand n t mu = Complex.exp (↑(4 * t) * cubicCoreExponent n mu)

theorem quarticCoreExponent_re (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : (quarticCoreExponent n mu).re = -(Cn3Torus.sqNormEdge n mu / 2) + quarticCorr n (matrixOfEdge n mu)

theorem cubicCoreExponent_re (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : (cubicCoreExponent n mu).re = -(Cn3Torus.sqNormEdge n mu / 2)

theorem correctedCoreIntegrand_sub_quarticCoreIntegrand_norm_eq (n t : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ‖correctedCoreIntegrand n t mu - quarticCoreIntegrand n t mu‖ = Real.exp (-2 * ↑t * Cn3Torus.sqNormEdge n mu + 4 * ↑t * quarticCorr n (matrixOfEdge n mu)) * ‖Complex.exp (↑(4 * t) * (Complex.I * ↑(quinticP5 n (matrixOfEdge n mu)))) - 1‖

Exact pointwise factorization of the repaired-to-quartic core difference.

theorem quarticCoreIntegrand_sub_cubicCoreIntegrand_norm_eq (n t : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ‖quarticCoreIntegrand n t mu - cubicCoreIntegrand n t mu‖ = Real.exp (-2 * ↑t * Cn3Torus.sqNormEdge n mu) * |Real.exp (4 * ↑t * quarticCorr n (matrixOfEdge n mu)) - 1|

Exact pointwise factorization of the quartic-to-cubic core difference.

theorem complex_exp_mul_I_sub_one_norm_le_abs (u : ℝ) : ‖Complex.exp (↑u * Complex.I) - 1‖ ≤ |u|

Real-phase Lipschitz bound: |e^{iu} - 1| ≤ |u|.