Intermediate Asymptotic Statements

This file contains the two intermediate asymptotic statements used to prove the paper's final count theorems:

• prop_primary_box
• normalizedCount_asymptotic

Unlike RequestProject.HadamardCn3ShortMain, this file records the normalized count and the normalized torus integral. The final count statements are kept in HadamardCn3ShortMain on purpose.

def paperNormalizedCount (n t : ℕ) : ℝ

The normalized count N_{n,4t} / 2^(4nt).

Equations

• paperNormalizedCount n t = ↑(hadamardCount n (4 * t)) / 2 ^ (4 * n * t)

def paperTargetIntegral (n t : ℕ) : ℝ

The raw torus integral whose normalized form computes paperNormalizedCount n t.

Equations

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

def paperNormalizedIntegral (n t : ℕ) : ℝ

The normalized torus integral representing paperNormalizedCount n t.

Equations

• paperNormalizedIntegral n t = 1 / (2 * Real.pi) ^ n.choose 2 * paperTargetIntegral n t

def paperMainScale (n t : ℕ) : ℝ

The Gaussian main scale A_n(t).

Equations

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

def paperMainTerm (n t : ℕ) : ℝ

The Gaussian main term for the normalized count.

Equations

• paperMainTerm n t = (1 - ↑(n.choose 3) / (8 * ↑t)) * paperMainScale n t

theorem paperNormalizedCount_eq_integral (n t : ℕ) : paperNormalizedCount n t = paperNormalizedIntegral n t

Fourier inversion bridge for the normalized count.

theorem prop_primary_box : ∃ (c : ℝ) (K : ℝ) (C : ℝ), 0 < c ∧ 0 < K ∧ 0 < C ∧ ∀ (n : ℕ), 3 ≤ n → ∀ (t : ℕ), ↑t ≥ C * ↑n ^ 3 → |primaryCoreContribution n t - paperMainTerm n t| ≤ (K * ↑n ^ 2 / ↑t + K * (↑n ^ (5 / 2) / ↑t ^ (3 / 2)) + K * ↑n ^ 6 / ↑t ^ 2 + K * Real.exp (-(c * ↑n ^ 2))) * paperMainScale n t

theorem normalizedCount_asymptotic : ∃ (c : ℝ) (K : ℝ) (C : ℝ), 0 < c ∧ 0 < K ∧ 0 < C ∧ ∀ (n : ℕ), 3 ≤ n → ∀ (t : ℕ), ↑t ≥ C * ↑n ^ 3 → |paperNormalizedCount n t - paperMainTerm n t| ≤ (K * ↑n ^ 2 / ↑t + K * (↑n ^ (5 / 2) / ↑t ^ (3 / 2)) + K * ↑n ^ 6 / ↑t ^ 2 + K * Real.exp (-(c * ↑n ^ 2))) * paperMainScale n t

Paper-facing normalized-count theorem on the Gaussian scale.

This upgrades prop_primary_box by adding the residual estimate, so the same explicit center controls the full normalized count N_{n,4t} / 2^{4nt}.