Foundational Definitions For The Cn^3 Formalization

This module contains the basic combinatorial, Gaussian, and coordinate-level objects used throughout the active development.

It is intentionally definition-heavy: the later analytic and counting bridges live in the split follow-on modules

• RequestProject.HadamardCn3TorusCount
• RequestProject.HadamardCn3Moments
• RequestProject.HadamardCn3MOO
• RequestProject.HadamardCn3ResidualBase

Architecture

We model edge data using symmetric matrices Fin n → Fin n → ℝ rather than an explicit Fin (n.choose 2) coordinate system. This keeps the basic definitions, influence statistics, and Gaussian support quantities closer to the mathematical notation used downstream.

Setup and Core Definitions

def dim (n : ℕ) : ℕ

The dimension d = n choose 2, the number of edges of the complete graph K_n.

Equations

• dim n = n.choose 2

def signOf (b : Fin 2) : ℤ

The set of all sign vectors in {-1,1}^n, represented via Fin 2. We encode: 0 ↦ -1, 1 ↦ 1.

Equations

• signOf b = 2 * ↑↑b - 1

def innerX (n : ℕ) (lam : Fin n → Fin n → ℝ) (σ : Fin n → Fin 2) : ℝ

The quadratic form X_λ(σ) = Σ_{i<j} λ_{ij} σ_i σ_j on sign vectors.

Equations

• innerX n lam σ = ∑ i : Fin n, ∑ j : Fin n, if i < j then lam i j * ↑(signOf (σ i)) * ↑(signOf (σ j)) else 0

def gaussianInnerX (n : ℕ) (lam : Fin n → Fin n → ℝ) (x : Fin n → ℝ) : ℝ

The same quadratic form evaluated on real coordinates, used for the Gaussian comparison side of the Mossel-O'Donnell-Oleszkiewicz invariance principle.

Equations

• gaussianInnerX n lam x = ∑ i : Fin n, ∑ j : Fin n, if i < j then lam i j * x i * x j else 0

def psi (n : ℕ) (lam : Fin n → Fin n → ℝ) : ℂ

The discrete Fourier average ψ_n(λ) = 2^{-n} Σ_{σ ∈ {-1,1}^n} exp(i X_λ(σ)).

Equations

• psi n lam = (↑(2 ^ n))⁻¹ * ∑ σ : Fin n → Fin 2, Complex.exp (Complex.I * ↑(innerX n lam σ))

def sNorm (n : ℕ) (lam : Fin n → Fin n → ℝ) : ℝ

s(λ) = ‖λ‖² = Σ_{i<j} λ_{ij}², the squared norm of the edge vector.

Equations

• sNorm n lam = ∑ i : Fin n, ∑ j : Fin n, if i < j then lam i j ^ 2 else 0

def cubicT (n : ℕ) (lam : Fin n → Fin n → ℝ) : ℝ

T(λ) = Σ_{i<j<k} λ_{ij} λ_{ik} λ_{jk}, the triangle sum.

Equations

• 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

def gaussianF (d : ℕ) (t : ℝ) : ℝ

The Gaussian integral F(d,t) = (π/(2t))^{d/2}.

Equations

• gaussianF d t = (Real.pi / (2 * t)) ^ (↑d / 2)

def coreMass (d : ℕ) (t : ℝ) : ℝ

The inner-core Gaussian mass G_core(d,t) = ∫_{‖λ‖²≤d/t} e^{-2t‖λ‖²} dλ. Defined as the Lebesgue integral with indicator.

Equations

• coreMass d t = ∫ (x : Fin d → ℝ), {x : Fin d → ℝ | ∑ i : Fin d, x i ^ 2 ≤ ↑d / t}.indicator (fun (x : Fin d → ℝ) => Real.exp (-2 * t * ∑ i : Fin d, x i ^ 2)) x

def hadamardCount (n s : ℕ) : ℕ

The number N_{n,s} of n × s partial Hadamard matrices. An n × s partial Hadamard matrix has entries ±1 with pairwise orthogonal rows.

Equations

• hadamardCount n s = {M : Fin n → Fin s → Fin 2 | ∀ (i j : Fin n), i ≠ j → ∑ k : Fin s, ↑(signOf (M i k)) * ↑(signOf (M j k)) = 0}.card

def normalizedCount (n s : ℕ) : ℝ

The normalized count N_{n,s} / 2^{ns}. This is the combinatorial quantity directly identified with the normalized torus integral.

Equations

• normalizedCount n s = ↑(hadamardCount n s) / 2 ^ (n * s)

def gaussianMatrix (n : ℕ) (lam : Fin n → Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

The symmetric zero-diagonal matrix attached to lam, obtained by reflecting the strict upper-triangular coordinates across the diagonal.

Equations

• gaussianMatrix n lam i j = edgeVal✝ lam i j

theorem gaussianMatrix_isHermitian (n : ℕ) (lam : Fin n → Fin n → ℝ) : (gaussianMatrix n lam).IsHermitian

theorem gaussianMatrix_eigenvalue_sq_sum (n : ℕ) (lam : Fin n → Fin n → ℝ) : let T := Matrix.toEuclideanLin (gaussianMatrix n lam); have hSymm := ⋯; ∑ i : Fin n, hSymm.eigenvalues ⋯ i ^ 2 = 2 * sNorm n lam

def simpleCycle4 (n : ℕ) (lam : Fin n → Fin n → ℝ) : ℝ

The simple 4-cycle sum over increasing quadruples of vertices.

Equations

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

def orderedCycle4 (n : ℕ) (lam : Fin n → Fin n → ℝ) : ℝ

The ordered 4-cycle form C_4^ord(λ) = Σ over ordered 4-cycles.

Equations

• orderedCycle4 n lam = 8 * simpleCycle4 n lam

def quarticCorr (n : ℕ) (lam : Fin n → Fin n → ℝ) : ℝ

The corrected quartic polynomial Q_4^corr(λ) = -(1/12) Σ_e λ_e⁴ + (1/8) C_4^ord(λ).

Equations

• quarticCorr n lam = (-(1 / 12) * ∑ i : Fin n, ∑ j : Fin n, if i < j then lam i j ^ 4 else 0) + 1 / 8 * orderedCycle4 n lam

def minorLamLast {n : ℕ} (lam : Fin (n + 1) → Fin (n + 1) → ℝ) : Fin n → Fin n → ℝ

The upper-left minor obtained by deleting the last vertex.

Equations

• minorLamLast lam i j = lam i.castSucc j.castSucc

def lastColLam {n : ℕ} (lam : Fin (n + 1) → Fin (n + 1) → ℝ) : Fin n → ℝ

The last-column edge weights obtained by deleting the last vertex.

Equations

• lastColLam lam i = lam i.castSucc (Fin.last n)

def simpleCycle4LastCross (n : ℕ) (B : Fin n → Fin n → ℝ) (x : Fin n → ℝ) : ℝ

The simple 4-cycle contribution coming from cycles that use the last vertex.

Equations

• simpleCycle4LastCross n B x = ∑ i : Fin n, ∑ j : Fin n, ∑ k : Fin n, if i < j ∧ j < k then B i j * B j k * x k * x i + B i j * x j * x k * B i k + B i k * B j k * x j * x i else 0

def cubicTLastCross (n : ℕ) (B : Fin n → Fin n → ℝ) (x : Fin n → ℝ) : ℝ

The triangle contribution coming from triangles that use the last vertex.

Equations

• cubicTLastCross n B x = ∑ i : Fin n, ∑ j : Fin n, if i < j then B i j * x i * x j else 0

theorem strictUpper_sum_split_last {n : ℕ} (f : Fin (n + 1) → Fin (n + 1) → ℝ) : (∑ i : Fin (n + 1), ∑ j : Fin (n + 1), if i < j then f i j else 0) = (∑ i : Fin n, ∑ j : Fin n, if i < j then f i.castSucc j.castSucc else 0) + ∑ i : Fin n, f i.castSucc (Fin.last n)

Split a strict upper-triangular double sum by whether the second index is the last vertex or not.

theorem sNorm_peel_last (n : ℕ) (lam : Fin (n + 1) → Fin (n + 1) → ℝ) : sNorm (n + 1) lam = sNorm n (minorLamLast lam) + ∑ i : Fin n, lastColLam lam i ^ 2

The squared edge norm splits into the peeled minor and the last column.

theorem cubicT_peel_last (n : ℕ) (lam : Fin (n + 1) → Fin (n + 1) → ℝ) : cubicT (n + 1) lam = cubicT n (minorLamLast lam) + cubicTLastCross n (minorLamLast lam) (lastColLam lam)

The triangle form splits by whether a triangle uses the last vertex.

theorem quarticCorr_peel_last (n : ℕ) (lam : Fin (n + 1) → Fin (n + 1) → ℝ) : quarticCorr (n + 1) lam = quarticCorr n (minorLamLast lam) + simpleCycle4LastCross n (minorLamLast lam) (lastColLam lam) - 1 / 12 * ∑ i : Fin n, lastColLam lam i ^ 4

Manuscript lem:quartic-peeling in corrected-quartic form.

def avgSigns (n : ℕ) (f : (Fin n → Fin 2) → ℝ) : ℝ

Averaging over all sign vectors in (Fin n → Fin 2).

Equations

• avgSigns n f = (↑(2 ^ n))⁻¹ * ∑ σ : Fin n → Fin 2, f σ

def stdGaussianAvg (n : ℕ) (f : (Fin n → ℝ) → ℝ) : ℝ

Expectation against the standard Gaussian law on ℝ^n, written as a normalized Lebesgue integral.

Equations

• stdGaussianAvg n f = ((2 * Real.pi) ^ (↑n / 2))⁻¹ * ∫ (x : Fin n → ℝ), f x * Real.exp ((-∑ i : Fin n, x i ^ 2) / 2)

Internal Gaussian characteristic-function support

def gaussianPsiIntegrand (n : ℕ) (lam : Fin n → Fin n → ℝ) (x : Fin n → ℝ) : ℂ

The complex Gaussian integrand for the quadratic phase gaussianInnerX.

Equations

• gaussianPsiIntegrand n lam x = Complex.exp (↑((-∑ i : Fin n, x i ^ 2) / 2) + ↑(gaussianInnerX n lam x) * Complex.I)

def gaussianPsiComplex (n : ℕ) (lam : Fin n → Fin n → ℝ) : ℂ

The complex-valued Gaussian characteristic function corresponding to gaussianInnerX.

Equations

• gaussianPsiComplex n lam = (∫ (x : Fin n → ℝ), gaussianPsiIntegrand n lam x) / ↑((2 * Real.pi) ^ (↑n / 2))

theorem integrable_stdGaussianDensity (n : ℕ) : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => Real.exp ((-∑ i : Fin n, x i ^ 2) / 2)) MeasureTheory.volume

def gaussianPsi (n : ℕ) (lam : Fin n → Fin n → ℝ) : ℂ

The Gaussian quadratic-characteristic function used in the MOO comparison, written via its real and imaginary parts: E[cos(gaussianInnerX)] + i E[sin(gaussianInnerX)]. This is the exact package needed to combine the MOO cosine/sine comparison with the Gaussian modulus estimate from the text.

Equations

• gaussianPsi n lam = ↑(stdGaussianAvg n fun (x : Fin n → ℝ) => Real.cos (gaussianInnerX n lam x)) + ↑(stdGaussianAvg n fun (x : Fin n → ℝ) => Real.sin (gaussianInnerX n lam x)) * Complex.I

theorem gaussianPsi_re (n : ℕ) (lam : Fin n → Fin n → ℝ) : (gaussianPsi n lam).re = stdGaussianAvg n fun (x : Fin n → ℝ) => Real.cos (gaussianInnerX n lam x)

theorem gaussianPsi_im (n : ℕ) (lam : Fin n → Fin n → ℝ) : (gaussianPsi n lam).im = stdGaussianAvg n fun (x : Fin n → ℝ) => Real.sin (gaussianInnerX n lam x)

theorem gaussianPsi_eq_gaussianPsiComplex (n : ℕ) (lam : Fin n → Fin n → ℝ) : gaussianPsi n lam = gaussianPsiComplex n lam

theorem gaussianInnerX_eq_half_inner_toEuclideanLin (n : ℕ) (lam : Fin n → Fin n → ℝ) (x : Fin n → ℝ) : gaussianInnerX n lam x = 1 / 2 * inner ℝ (WithLp.toLp 2 x) ((Matrix.toEuclideanLin (gaussianMatrix n lam)) (WithLp.toLp 2 x))

def momentX (n : ℕ) (lam : Fin n → Fin n → ℝ) (k : ℕ) : ℝ

The k-th moment of X_λ over Rademacher signs: μ_k(λ) = E[X_λ^k].

Equations

• momentX n lam k = (↑(2 ^ n))⁻¹ * ∑ σ : Fin n → Fin 2, innerX n lam σ ^ k

theorem continuous_momentX (n k : ℕ) : Continuous fun (lam : Fin n → Fin n → ℝ) => momentX n lam k

The matrix-model moments vary continuously with the edge weights.

theorem continuous_cubicT (n : ℕ) : Continuous (cubicT n)

The cubic triangle sum is a continuous polynomial in the matrix entries.

def linearX (n : ℕ) (x : Fin n → ℝ) (σ : Fin n → Fin 2) : ℝ

Linear Rademacher form on vertex weights.

Equations

• linearX n x σ = ∑ i : Fin n, x i * ↑(signOf (σ i))

def singleEdgeLam {n : ℕ} (u v : Fin n) : Fin n → Fin n → ℝ

The strict-upper indicator supported on a single edge (u,v).

Equations

• singleEdgeLam u v i j = if i = u ∧ j = v then 1 else 0

def triangleThroughPair (n : ℕ) (B : Fin n → Fin n → ℝ) (u v : Fin n) : ℝ

Sum of the two-edge products over triangles containing the ordered pair (u,v).

Equations

• triangleThroughPair n B u v = ((∑ k : Fin n, if k < u then B k u * B k v else 0) + ∑ k : Fin n, if u < k ∧ k < v then B u k * B k v else 0) + ∑ k : Fin n, if v < k then B u k * B v k else 0

Internal last-coordinate peeling identities

theorem sum_signVec_split_last (n : ℕ) (g : (Fin (n + 1) → Fin 2) → ℝ) : ∑ τ : Fin (n + 1) → Fin 2, g τ = ∑ σ : Fin n → Fin 2, ∑ b : Fin 2, g (Fin.snoc σ b)

Expand a sum over sign vectors on Fin (n+1) by the last coordinate.

theorem avgSigns_split_last (n : ℕ) (g : (Fin (n + 1) → Fin 2) → ℝ) : avgSigns (n + 1) g = avgSigns n fun (σ : Fin n → Fin 2) => (∑ b : Fin 2, g (Fin.snoc σ b)) / 2

Average over sign vectors by first averaging over the last sign.

theorem linearX_snoc_last (n : ℕ) (x : Fin n → ℝ) (a : ℝ) (σ : Fin n → Fin 2) (b : Fin 2) : linearX (n + 1) (Fin.snoc x a) (Fin.snoc σ b) = linearX n x σ + a * ↑(signOf b)

theorem signOf_sq (b : Fin 2) : ↑(signOf b) ^ 2 = 1

theorem sum_linear_over_last_sign (A Y : ℝ) : ∑ b : Fin 2, (A + ↑(signOf b) * Y) = 2 * A

theorem sum_square_over_last_sign (A Y : ℝ) : ∑ b : Fin 2, (A + ↑(signOf b) * Y) ^ 2 = 2 * (A ^ 2 + Y ^ 2)

theorem sum_cube_over_last_sign (A Y : ℝ) : ∑ b : Fin 2, (A + ↑(signOf b) * Y) ^ 3 = 2 * (A ^ 3 + 3 * A * Y ^ 2)

theorem sum_sq_snoc (n : ℕ) (x : Fin n → ℝ) (a : ℝ) : ∑ i : Fin (n + 1), Fin.snoc x a i ^ 2 = ∑ i : Fin n, x i ^ 2 + a ^ 2

theorem sum_fourth_snoc (n : ℕ) (x : Fin n → ℝ) (a : ℝ) : ∑ i : Fin (n + 1), Fin.snoc x a i ^ 4 = ∑ i : Fin n, x i ^ 4 + a ^ 4

theorem innerX_snoc_last (n : ℕ) (lam : Fin (n + 1) → Fin (n + 1) → ℝ) (σ : Fin n → Fin 2) (b : Fin 2) : innerX (n + 1) lam (Fin.snoc σ b) = innerX n (minorLamLast lam) σ + ↑(signOf b) * linearX n (lastColLam lam) σ

theorem sum_fourth_over_last_sign (A Y : ℝ) : ∑ b : Fin 2, (A + ↑(signOf b) * Y) ^ 4 = 2 * (A ^ 4 + 6 * A ^ 2 * Y ^ 2 + Y ^ 4)

theorem sum_sixth_over_last_sign (A Y : ℝ) : ∑ b : Fin 2, (A + ↑(signOf b) * Y) ^ 6 = 2 * (A ^ 6 + 15 * A ^ 4 * Y ^ 2 + 15 * A ^ 2 * Y ^ 4 + Y ^ 6)

theorem sum_eighth_over_last_sign (A Y : ℝ) : ∑ b : Fin 2, (A + ↑(signOf b) * Y) ^ 8 = 2 * (A ^ 8 + 28 * A ^ 6 * Y ^ 2 + 70 * A ^ 4 * Y ^ 4 + 28 * A ^ 2 * Y ^ 6 + Y ^ 8)

theorem avgSigns_congr (n : ℕ) {f g : (Fin n → Fin 2) → ℝ} (hfg : ∀ (σ : Fin n → Fin 2), f σ = g σ) : avgSigns n f = avgSigns n g

theorem avgSigns_const_aux (n : ℕ) (c : ℝ) : (avgSigns n fun (x : Fin n → Fin 2) => c) = c

theorem avgSigns_add_aux (n : ℕ) (f g : (Fin n → Fin 2) → ℝ) : (avgSigns n fun (σ : Fin n → Fin 2) => f σ + g σ) = avgSigns n f + avgSigns n g

theorem avgSigns_cos_sq_linearX_eq_half_one_add_half_prod (n : ℕ) (x : Fin n → ℝ) : (avgSigns n fun (σ : Fin n → Fin 2) => Real.cos (linearX n x σ) ^ 2) = 1 / 2 + 1 / 2 * ∏ i : Fin n, Real.cos (2 * x i)

theorem momentX_four_peel_last_raw (n : ℕ) (lam : Fin (n + 1) → Fin (n + 1) → ℝ) : momentX (n + 1) lam 4 = avgSigns n fun (σ : Fin n → Fin 2) => innerX n (minorLamLast lam) σ ^ 4 + 6 * innerX n (minorLamLast lam) σ ^ 2 * linearX n (lastColLam lam) σ ^ 2 + linearX n (lastColLam lam) σ ^ 4

theorem abs_pow_even (x : ℝ) (k : ℕ) : |x| ^ (2 * k) = x ^ (2 * k)

def quinticP5 (n : ℕ) (lam : Fin n → Fin n → ℝ) : ℝ

The 5th cumulant phase P_5(λ) = κ_5(λ)/120. Using the moment-cumulant relation (for zero-mean): κ_5 = μ_5 - 10·μ_3·μ_2.

Equations

• quinticP5 n lam = (momentX n lam 5 - 10 * momentX n lam 3 * momentX n lam 2) / 120

theorem continuous_quinticP5 (n : ℕ) : Continuous (quinticP5 n)

The quintic correction is a continuous polynomial in the matrix entries.

def gaussianScale (n : ℕ) (t : ℝ) : ℝ

The Gaussian scale A_n(t) = 2^{2d-n+1} (8πt)^{-d/2}.

Equations

• gaussianScale n t = 2 ^ (2 * ↑(dim n) - ↑n + 1) * (8 * Real.pi * t) ^ (-↑(dim n) / 2)

def countScale (n t : ℕ) : ℝ

The count scale 2^{4nt} A_n(t) appearing in cor:cn3-count-asym.

Equations

• countScale n t = 2 ^ (4 * n * t) * gaussianScale n ↑t

theorem gaussianScale_pos (n : ℕ) {t : ℝ} (ht : 0 < t) : 0 < gaussianScale n t