Torus / Count Bridge For The Cn^3 Formalization

This module contains the torus-coordinate model, the Fourier inversion bridge, and the normalized-count identification used throughout the formalization.

Readers primarily interested in the combinatorial-to-analytic translation should start with:

• Cn3Torus.lem_fourier_inversion_all
• torusIntegralC_eq_volume_mul_hadamardCount
• normalizedCount_eq_normalizedTargetIntegral

def Cn3Torus.d (n : ℕ) : ℕ

Edge-coordinate dimension.

Equations

• Cn3Torus.d n = n.choose 2

def Cn3Torus.Edge (n : ℕ) : Type

Strict upper-triangular coordinates, viewed as edges of K_n.

Equations

• Cn3Torus.Edge n = { p : Fin n × Fin n // p.1 < p.2 }

instance Cn3Torus.instFintypeEdge (n : ℕ) : Fintype (Edge n)

Equations

• Cn3Torus.instFintypeEdge n = id inferInstance

instance Cn3Torus.instDecidableEqEdge (n : ℕ) : DecidableEq (Edge n)

Equations

• Cn3Torus.instDecidableEqEdge n = id inferInstance

noncomputable def Cn3Torus.edgeToSym2Subtype {n : ℕ} (e : Edge n) : { a : Sym2 (Fin n) // ¬a.IsDiag }

Identify an edge with the corresponding non-diagonal unordered pair.

Equations

• Cn3Torus.edgeToSym2Subtype e = ⟨s((↑e).1, (↑e).2), ⋯⟩

theorem Cn3Torus.card_Edge_eq_d (n : ℕ) : Fintype.card (Edge n) = d n

The edge-coordinate space has dimension n.choose 2.

def Cn3Torus.spin (b : Bool) : ℝ

Boolean spin encoding, matching the edge-model torus setup.

Equations

• Cn3Torus.spin b = if b = true then 1 else -1

def Cn3Torus.Z {n : ℕ} (y : Fin n → Bool) : Edge n → ℝ

Edge monomials attached to a Boolean sign vector.

Equations

• Cn3Torus.Z y e = Cn3Torus.spin (y (↑e).1) * Cn3Torus.spin (y (↑e).2)

def Cn3Torus.phase {n : ℕ} (lam : Edge n → ℝ) (y : Fin n → Bool) : ℝ

The edge-model phase.

Equations

• Cn3Torus.phase lam y = ∑ e : Cn3Torus.Edge n, lam e * Cn3Torus.Z y e

def Cn3Torus.psi (n : ℕ) (lam : Edge n → ℝ) : ℂ

Edge-model characteristic function.

Equations

• Cn3Torus.psi n lam = (∑ y : Fin n → Bool, Complex.exp (Complex.I * ↑(Cn3Torus.phase lam y))) / 2 ^ n

theorem Cn3Torus.continuous_psi (n : ℕ) : Continuous (psi n)

def Cn3Torus.sqNormEdge (n : ℕ) (lam : Edge n → ℝ) : ℝ

Edge-model squared norm.

Equations

• Cn3Torus.sqNormEdge n lam = ∑ e : Cn3Torus.Edge n, lam e ^ 2

theorem Cn3Torus.continuous_sqNormEdge (n : ℕ) : Continuous (sqNormEdge n)

def Cn3Torus.torusBox (n : ℕ) : Set (Edge n → ℝ)

The torus fundamental box of side length 2π in edge coordinates.

Equations

• Cn3Torus.torusBox n = Set.univ.pi fun (x : Cn3Torus.Edge n) => Set.Icc (-(Real.pi / 4)) (7 * Real.pi / 4)

def Cn3Torus.torusIntegralC (n m : ℕ) : ℂ

Complex torus integral before taking real parts.

Equations

• Cn3Torus.torusIntegralC n m = ∫ (lam : Cn3Torus.Edge n → ℝ) in Cn3Torus.torusBox n, Cn3Torus.psi n lam ^ m

def Cn3Torus.targetIntegral (n t : ℕ) : ℝ

Real quarter-scale torus integral.

Equations

• Cn3Torus.targetIntegral n t = ∫ (lam : Cn3Torus.Edge n → ℝ) in Cn3Torus.torusBox n, (Cn3Torus.psi n lam ^ (4 * t)).re

def Cn3Torus.normalizedTargetIntegral (n t : ℕ) : ℝ

Torus integral normalized by the torus volume (2π)^d.

Equations

• Cn3Torus.normalizedTargetIntegral n t = 1 / (2 * Real.pi) ^ Cn3Torus.d n * Cn3Torus.targetIntegral n t

def Cn3Torus.edgeCount (n : ℕ) : ℝ

Edge-count as a real number.

Equations

• Cn3Torus.edgeCount n = ↑(Fintype.card (Cn3Torus.Edge n))

def Cn3Torus.delta : ℝ

Fixed local radius used in the torus decomposition package.

Equations

• Cn3Torus.delta = 3 * Real.pi / 16

theorem Cn3Torus.delta_pos : 0 < delta

def Cn3Torus.localBox (n : ℕ) : Set (Edge n → ℝ)

Local box around a lattice point in edge coordinates.

Equations

• Cn3Torus.localBox n = Set.univ.pi fun (x : Cn3Torus.Edge n) => Set.Icc (-Cn3Torus.delta) Cn3Torus.delta

theorem Cn3Torus.sqNormEdge_coord_sq_le (n : ℕ) (lam : Edge n → ℝ) (e : Edge n) : lam e ^ 2 ≤ sqNormEdge n lam

A single coordinate square is bounded by the total edge squared norm.

theorem Cn3Torus.localBox_isCompact (n : ℕ) : IsCompact (localBox n)

def Cn3Torus.localIntegral (n t : ℕ) : ℝ

Local integral over the core box.

Equations

• Cn3Torus.localIntegral n t = ∫ (lam : Cn3Torus.Edge n → ℝ) in Cn3Torus.localBox n, (Cn3Torus.psi n lam ^ (4 * t)).re

def Cn3Torus.texPrefactor (n : ℕ) : ℝ

The tex prefactor converting local integrals to normalized torus scale.

Equations

• Cn3Torus.texPrefactor n = 2 ^ (2 * Cn3Torus.d n - n + 1) / (2 * Real.pi) ^ Cn3Torus.d n

theorem Cn3Torus.n_le_two_mul_d (n : ℕ) (hn : 3 ≤ n) : n ≤ 2 * d n

theorem Cn3Torus.lem_fourier_inversion_all (n m : ℕ) : (torusIntegralC n m).re = ∫ (lam : Edge n → ℝ) in torusBox n, (psi n lam ^ m).re

Fourier inversion on the quarter-scale torus model.

This identifies the real-valued target integral used in the paper with the real part of the complex torus integral torusIntegralC.

@[reducible, inline]

abbrev Cn3Torus.EdgeNe {n : ℕ} (e0 : Edge n) : Type

Equations

• Cn3Torus.EdgeNe e0 = { e : Cn3Torus.Edge n // e ≠ e0 }

theorem Cn3Torus.pow_nat_le_nat_pow_mul_exp {u : ℝ} (m : ℕ) (hm : 0 < m) (hu : 0 ≤ u) : u ^ m ≤ ↑m ^ m * Real.exp u

A coarse but convenient domination of polynomial growth by a single exponential.

theorem Cn3Torus.log_two_lt_three_quarters : Real.log 2 < 3 / 4

theorem Cn3Torus.log_nat_lt_half (n : ℕ) (hn : 3 ≤ n) : Real.log ↑n < ↑n / 2

def Cn3Torus.avgOver (n : ℕ) (f : (Fin n → Bool) → ℝ) : ℝ

Averaging over all Boolean sign vectors.

Equations

• Cn3Torus.avgOver n f = (∑ y : Fin n → Bool, f y) / 2 ^ n

theorem Cn3Torus.avgOver_const (n : ℕ) (c : ℝ) : (avgOver n fun (x : Fin n → Bool) => c) = c

def Cn3Torus.W {n : ℕ} (mu : Edge n → ℝ) (y : Fin n → Bool) : ℝ

The edge-model polynomial W, equal to phase.

Equations

• Cn3Torus.W mu y = ∑ e : Cn3Torus.Edge n, mu e * Cn3Torus.Z y e

theorem Cn3Torus.phase_eq_W {n : ℕ} (mu : Edge n → ℝ) (y : Fin n → Bool) : phase mu y = W mu y

def Cn3Torus.edgesIncident (n : ℕ) (i : Fin n) : Finset (Edge n)

The edges incident to a given vertex.

Equations

• Cn3Torus.edgesIncident n i = {e : Cn3Torus.Edge n | (↑e).1 = i ∨ (↑e).2 = i}

theorem Cn3Torus.mem_edgesIncident_iff {n : ℕ} {i : Fin n} {e : Edge n} : e ∈ edgesIncident n i ↔ (↑e).1 = i ∨ (↑e).2 = i

theorem Cn3Torus.edge_mem_edgesIncident_left {n : ℕ} (e : Edge n) : e ∈ edgesIncident n (↑e).1

theorem Cn3Torus.edge_mem_edgesIncident_right {n : ℕ} (e : Edge n) : e ∈ edgesIncident n (↑e).2

def Cn3Torus.flipBoolAt {n : ℕ} (i : Fin n) (y : Fin n → Bool) : Fin n → Bool

Flip the Boolean sign at a single vertex.

Equations

• Cn3Torus.flipBoolAt i y j = if j = i then !y j else y j

theorem Cn3Torus.Z_sq_eq_one {n : ℕ} (y : Fin n → Bool) (e : Edge n) : Z y e ^ 2 = 1

theorem Cn3Torus.Z_flip_at {n : ℕ} (i : Fin n) (y : Fin n → Bool) (e : Edge n) : Z (flipBoolAt i y) e = if e ∈ edgesIncident n i then -Z y e else Z y e

theorem Cn3Torus.sum_flipBoolAt_eq {n : ℕ} {β : Type u_1} [AddCommMonoid β] (i : Fin n) (f : (Fin n → Bool) → β) : ∑ y : Fin n → Bool, f (flipBoolAt i y) = ∑ y : Fin n → Bool, f y

def Cn3Torus.edgeNatRowSum {n : ℕ} (b : Edge n → ℕ) (i : Fin n) : ℕ

Row-degree of an edge monomial at vertex i.

Equations

• Cn3Torus.edgeNatRowSum b i = ∑ e ∈ Cn3Torus.edgesIncident n i, b e

def Cn3Torus.edgeZMonomial {n : ℕ} (b : Edge n → ℕ) (y : Fin n → Bool) : ℝ

Edge monomial in the sign variables.

Equations

• Cn3Torus.edgeZMonomial b y = ∏ e : Cn3Torus.Edge n, Cn3Torus.Z y e ^ b e

theorem Cn3Torus.avg_edgeZMonomial_eq_ite_allEven {n : ℕ} (b : Edge n → ℕ) : (avgOver n fun (y : Fin n → Bool) => edgeZMonomial b y) = if ∀ (i : Fin n), Even (edgeNatRowSum b i) then 1 else 0

def Cn3Torus.edgeMultiplicity4 {n : ℕ} (e₁ e₂ e₃ e₄ : Edge n) : Edge n → ℕ

Edge multiplicities attached to an ordered 4-tuple of edges.

Equations

• Cn3Torus.edgeMultiplicity4 e₁ e₂ e₃ e₄ e = (((if e = e₁ then 1 else 0) + if e = e₂ then 1 else 0) + if e = e₃ then 1 else 0) + if e = e₄ then 1 else 0

theorem Cn3Torus.edgeZMonomial_add {n : ℕ} (b₁ b₂ : Edge n → ℕ) (y : Fin n → Bool) : edgeZMonomial (fun (e : Edge n) => b₁ e + b₂ e) y = edgeZMonomial b₁ y * edgeZMonomial b₂ y

theorem Cn3Torus.edgeZMonomial_single {n : ℕ} (y : Fin n → Bool) (e₀ : Edge n) : edgeZMonomial (fun (e : Edge n) => if e = e₀ then 1 else 0) y = Z y e₀

theorem Cn3Torus.edgeZMonomial_edgeMultiplicity4 {n : ℕ} (y : Fin n → Bool) (e₁ e₂ e₃ e₄ : Edge n) : edgeZMonomial (edgeMultiplicity4 e₁ e₂ e₃ e₄) y = Z y e₁ * Z y e₂ * Z y e₃ * Z y e₄

theorem Cn3Torus.exists_incident_xor_of_ne {n : ℕ} {e f : Edge n} (hef : e ≠ f) : ∃ (i : Fin n), e ∈ edgesIncident n i ∧ f ∉ edgesIncident n i ∨ f ∈ edgesIncident n i ∧ e ∉ edgesIncident n i

instance Cn3Torus.instFintypeLambdaCode (n : ℕ) : Fintype (Cn3Torus.LambdaCode✝ n)

Equations

• Cn3Torus.instFintypeLambdaCode n = id inferInstance

instance Cn3Torus.instDecidableEqLambdaCode (n : ℕ) : DecidableEq (Cn3Torus.LambdaCode✝ n)

Equations

• Cn3Torus.instDecidableEqLambdaCode n = id inferInstance

instance Cn3Torus.instDecidablePredRowParityEven (n : ℕ) : DecidablePred Cn3Torus.rowParityEven✝

Equations

• Cn3Torus.instDecidablePredRowParityEven n b = id inferInstance

instance Cn3Torus.instDecidablePredParityEvenBool (n : ℕ) : DecidablePred Cn3Torus.parityEvenBool✝

Equations

• Cn3Torus.instDecidablePredParityEvenBool n p = id inferInstance

def Cn3Torus.lambdaShifts (n : ℕ) : Finset (Edge n → ℝ)

Equations

• Cn3Torus.lambdaShifts n = Finset.image (fun (b : Cn3Torus.LambdaCode✝ n) => Cn3Torus.lambdaReal✝ b) (Cn3Torus.lambdaCodes✝ n)

theorem Cn3Torus.card_lambdaShifts_eq_pow_of_two_le (n : ℕ) (hn : 2 ≤ n) : (lambdaShifts n).card = 2 ^ (2 * d n - n + 1)

theorem Cn3Torus.delta_lt_pi_div_four : delta < Real.pi / 4

Edge Coordinate Transport

The public transport maps edgeLam and matrixOfEdge identify matrix and edge coordinates. The Boolean-encoding conversions below are kept internal so the reader sees the transport results rather than the implementation vocabulary.

def signVecToBoolVec {n : ℕ} (σ : Fin n → Fin 2) : Fin n → Bool

Pointwise transport of sign vectors to the Bool-valued edge model.

Equations

• signVecToBoolVec σ i = fin2ToBool✝ (σ i)

def signVecEquivBoolVec (n : ℕ) : (Fin n → Fin 2) ≃ (Fin n → Bool)

Equivalence between the two encodings of sign vectors.

Equations

• signVecEquivBoolVec n = { toFun := signVecToBoolVec, invFun := boolVecToSignVec✝, left_inv := ⋯, right_inv := ⋯ }

def edgeLam (n : ℕ) (lam : Fin n → Fin n → ℝ) : Cn3Torus.Edge n → ℝ

Read a strict upper-triangular matrix as an edge-indexed function.

Equations

• edgeLam n lam e = lam (↑e).1 (↑e).2

def matrixOfEdge (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : Fin n → Fin n → ℝ

Embed edge coordinates back into the strict upper-triangular matrix model.

Equations

• matrixOfEdge n mu i j = if hij : i < j then mu ⟨(i, j), hij⟩ else 0

theorem continuous_matrixOfEdge (n : ℕ) : Continuous (matrixOfEdge n)

Edge-to-matrix transport is continuous coordinatewise.

theorem edgeLam_matrixOfEdge (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : edgeLam n (matrixOfEdge n mu) = mu

theorem spin_fin2ToBool_eq_signOf (b : Fin 2) : Cn3Torus.spin (fin2ToBool✝ b) = ↑(signOf b)

theorem dim_eq_edgeDim (n : ℕ) : dim n = Cn3Torus.d n

theorem card_Edge_eq_dim (n : ℕ) : Fintype.card (Cn3Torus.Edge n) = dim n

theorem sNorm_eq_sqNormEdge (n : ℕ) (lam : Fin n → Fin n → ℝ) : sNorm n lam = Cn3Torus.sqNormEdge n (edgeLam n lam)

theorem innerX_eq_edgePhase (n : ℕ) (lam : Fin n → Fin n → ℝ) (σ : Fin n → Fin 2) : innerX n lam σ = Cn3Torus.phase (edgeLam n lam) (signVecToBoolVec σ)

theorem sNorm_matrixOfEdge_eq (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : sNorm n (matrixOfEdge n mu) = Cn3Torus.sqNormEdge n mu

theorem psi_matrixOfEdge_eq (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : psi n (matrixOfEdge n mu) = Cn3Torus.psi n mu

theorem torusIntegralC_eq_volume_mul_hadamardCount (n s : ℕ) : Cn3Torus.torusIntegralC n s = ↑((2 * Real.pi) ^ Cn3Torus.d n) * ↑(hadamardCount n s) / (2 ^ n) ^ s

Exact count-to-integral bridge for the torus model.

The torus integral equals the torus volume times the number of n × s partial Hadamard matrices, divided by the ambient sign count 2^(ns). This is the formal Fourier-inversion step connecting the combinatorial count to the analytic integral.

def Cn3Torus.edgeFromOffdiag {n : ℕ} (i : Fin n) (j : { k : Fin n // k ≠ i }) : Edge n

Equations

• Cn3Torus.edgeFromOffdiag i j = if hij : i < ↑j then ⟨(i, ↑j), hij⟩ else ⟨(↑j, i), ⋯⟩

def Cn3Torus.offdiagOfIncident {n : ℕ} (i : Fin n) (e : Edge n) (he : e ∈ edgesIncident n i) : { k : Fin n // k ≠ i }

Equations

• Cn3Torus.offdiagOfIncident i e he = if hleft : (↑e).1 = i then ⟨(↑e).2, ⋯⟩ else ⟨(↑e).1, hleft⟩

theorem Cn3Torus.edgeFromOffdiag_offdiagOfIncident {n : ℕ} (i : Fin n) (e : Edge n) (he : e ∈ edgesIncident n i) : edgeFromOffdiag i (offdiagOfIncident i e he) = e

theorem momentX_eq_avgOver_W_pow (n : ℕ) (lam : Fin n → Fin n → ℝ) (k : ℕ) : momentX n lam k = Cn3Torus.avgOver n fun (y : Fin n → Bool) => Cn3Torus.W (edgeLam n lam) y ^ k

theorem avgSigns_abs_innerX_pow_eq_avgOver_abs_W_pow (n : ℕ) (lam : Fin n → Fin n → ℝ) (k : ℕ) : (avgSigns n fun (σ : Fin n → Fin 2) => |innerX n lam σ| ^ k) = Cn3Torus.avgOver n fun (y : Fin n → Bool) => |Cn3Torus.W (edgeLam n lam) y| ^ k

def box (n : ℕ) (delta : ℝ) : Set (Fin n → Fin n → ℝ)

The box B_δ = {λ : |λ_{ij}| ≤ δ for all i < j}.

Equations

• box n delta = {lam : Fin n → Fin n → ℝ | ∀ (i j : Fin n), i < j → |lam i j| ≤ delta}

def coreRegion (n : ℕ) (t : ℝ) : Set (Fin n → Fin n → ℝ)

The inner-core region D_t = {λ : s(λ) ≤ d/t}.

Equations

• coreRegion n t = {lam : Fin n → Fin n → ℝ | sNorm n lam ≤ ↑(dim n) / t}

def edgeBox (n : ℕ) (delta : ℝ) : Set (Cn3Torus.Edge n → ℝ)

Edge-coordinate transport of the prototype box B_δ.

Equations

• edgeBox n delta = {mu : Cn3Torus.Edge n → ℝ | matrixOfEdge n mu ∈ box n delta}

def edgeEuclidBall (n : ℕ) (r : ℝ) : Set (Cn3Torus.Edge n → ℝ)

Edge-coordinate transport of the Euclidean ball D_r.

Equations

• edgeEuclidBall n r = {mu : Cn3Torus.Edge n → ℝ | matrixOfEdge n mu ∈ euclidBall'✝ n r}

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

Edge-coordinate transport of the core region D_t.

Equations

• edgeCoreRegion n t = {mu : Cn3Torus.Edge n → ℝ | matrixOfEdge n mu ∈ coreRegion n t}

def edgeEvenFarShell (n : ℕ) (r : ℝ) : Set (Cn3Torus.Edge n → ℝ)

Edge-coordinate transport of the even far shell.

Equations

• edgeEvenFarShell n r = {mu : Cn3Torus.Edge n → ℝ | matrixOfEdge n mu ∈ evenFarShell✝ n r}

theorem edgeBox_eq_pi (n : ℕ) (delta : ℝ) : edgeBox n delta = Set.univ.pi fun (x : Cn3Torus.Edge n) => Set.Icc (-delta) delta

theorem edgeBox_isCompact (n : ℕ) (delta : ℝ) : IsCompact (edgeBox n delta)

theorem edgeBox_volume_eq (n : ℕ) (delta : ℝ) (hdelta : 0 ≤ delta) : MeasureTheory.volume (edgeBox n delta) = ENNReal.ofReal ((2 * delta) ^ dim n)

def Cn3Torus.edgeResidualTorusRegion (n : ℕ) (delta : ℝ) : Set (Edge n → ℝ)

Residual torus region left after removing all translated primary boxes.

Equations

• Cn3Torus.edgeResidualTorusRegion n delta = Cn3Torus.torusBox n \ Cn3Torus.edgePrimaryBoxUnion✝ n delta

theorem mem_edgeEuclidBall_iff (n : ℕ) (r : ℝ) (mu : Cn3Torus.Edge n → ℝ) : mu ∈ edgeEuclidBall n r ↔ Cn3Torus.sqNormEdge n mu ≤ r ^ 2

theorem mem_edgeCoreRegion_iff (n : ℕ) (t : ℝ) (mu : Cn3Torus.Edge n → ℝ) : mu ∈ edgeCoreRegion n t ↔ Cn3Torus.sqNormEdge n mu ≤ ↑(dim n) / t

theorem measurableSet_edgeEuclidBall (n : ℕ) (r : ℝ) : MeasurableSet (edgeEuclidBall n r)

theorem measurableSet_edgeCoreRegion (n : ℕ) (t : ℝ) : MeasurableSet (edgeCoreRegion n t)

theorem mem_edgeEvenFarShell_iff (n : ℕ) (r : ℝ) (mu : Cn3Torus.Edge n → ℝ) : mu ∈ edgeEvenFarShell n r ↔ mu ∈ edgeBox n (Real.pi / 4) ∧ r ^ 2 ≤ Cn3Torus.sqNormEdge n mu

Fourier Inversion and Count Bridge

This section packages the de Launey-Levin quarter-scale Fourier bridge in the form used by the rest of the active development.

theorem normalizedCount_eq_normalizedTargetIntegral (n t : ℕ) : normalizedCount n (4 * t) = Cn3Torus.normalizedTargetIntegral n t

Fact 2.3 [DL10]: quarter-scale Fourier inversion in the edge-coordinate torus model. This is the exact bridge from the combinatorial normalized count to the normalized torus integral.

theorem universal_magnitude_bound_full (n : ℕ) (hn : 2 ≤ n) (gam : Fin n → Fin n → ℝ) (k : Fin n) : ‖psi n gam‖ ^ 2 ≤ 1 / 2 + 1 / 2 * ∏ i : Fin n, if i = k then 1 else if i < k then Real.cos (2 * gam i k) else Real.cos (2 * gam k i)

Fact 3.3 [DL10]: Full magnitude bound with product.

theorem avgSigns_mul_sq_le_avgSigns_sq_mul_avgSigns_sq (n : ℕ) (u v : (Fin n → Fin 2) → ℝ) : (avgSigns n fun (σ : Fin n → Fin 2) => u σ * v σ) ^ 2 ≤ (avgSigns n fun (σ : Fin n → Fin 2) => u σ ^ 2) * avgSigns n fun (σ : Fin n → Fin 2) => v σ ^ 2

theorem fixedDegreeHC_degree2_W_sixth (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : (Cn3Torus.avgOver n fun (y : Fin n → Bool) => |Cn3Torus.W mu y| ^ 6) ≤ 5 ^ 6 * Cn3Torus.sqNormEdge n mu ^ 3

Manuscript Fact 4.5(i): the degree-2 chaos W satisfies the L^6 hypercontractive bound with constant 5^6.

theorem fixedDegreeHC_degree2_W_seventh_uniform (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : (Cn3Torus.avgOver n fun (y : Fin n → Bool) => |Cn3Torus.W mu y| ^ 7) ≤ 6 ^ 7 * Cn3Torus.sqNormEdge n mu ^ (7 / 2)

theorem normalized_edgeResidualTorusRegion_abs_le_cos_pow (n t : ℕ) (hn : 2 ≤ n) {deltaBox : ℝ} (hdelta_pos : 0 < deltaBox) (hdelta_lt : deltaBox < Real.pi / 4) : |1 / (2 * Real.pi) ^ Cn3Torus.d n * ∫ (lam : Cn3Torus.Edge n → ℝ) in Cn3Torus.edgeResidualTorusRegion n deltaBox, (Cn3Torus.psi n lam ^ (4 * t)).re| ≤ Real.cos deltaBox ^ (4 * t)

theorem normalizedCount_primary_secondary_decomposition (n t : ℕ) {delta : ℝ} (hdelta_lt : delta < Real.pi / 4) : normalizedCount n (4 * t) = (↑(Cn3Torus.lambdaShifts n).card / (2 * Real.pi) ^ Cn3Torus.d n * ∫ (mu : Cn3Torus.Edge n → ℝ) in edgeBox n delta, (Cn3Torus.psi n mu ^ (4 * t)).re) + 1 / (2 * Real.pi) ^ Cn3Torus.d n * ∫ (mu : Cn3Torus.Edge n → ℝ) in Cn3Torus.edgeResidualTorusRegion n delta, (Cn3Torus.psi n mu ^ (4 * t)).re

The actual primary-secondary torus decomposition from the manuscript, written in edge coordinates and normalized directly at the normalized-count scale.

theorem normalizedCount_sub_texPrefactor_mul_localIntegral_abs_le_exp_neg_half_t (n t : ℕ) (hn : 2 ≤ n) : |normalizedCount n (4 * t) - Cn3Torus.texPrefactor n * Cn3Torus.localIntegral n t| ≤ Real.exp (-↑t / 2)

The global normalized count is within the exponentially small Rdelta error of the transported local-box contribution.