Paper-Facing Count Theorems

This file contains only the final count-facing statements from the arXiv paper https://arxiv.org/pdf/2603.30013.

The reader-facing quantities are:

• paperCount n s = N_{n,s}, the number of n × s partial Hadamard matrices
• paperAsymptoticCount n t = A_{n,4t}, the asymptotic scale from the paper

The endpoint theorems are:

• thm_main_intro, the formal analogue of Theorem \ref{thm:main-intro}
• cor_uniform, the formal analogue of Corollary \ref{cor:uniform}

The intermediate normalized-count and integral statements live in RequestProject.HadamardCn3Asymptotics.

def paperCount (n s : ℕ) : ℕ

Paper notation N_{n,s}: the number of n × s partial Hadamard matrices.

Equations

• paperCount 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 paperAsymptoticCount (n t : ℕ) : ℝ

Paper notation A_{n,4t} for the asymptotic count scale.

Equations

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

theorem thm_main_intro : ∃ (c : ℝ) (K : ℝ) (C : ℝ), 0 < c ∧ 0 < K ∧ 0 < C ∧ ∀ (n : ℕ), 3 ≤ n → ∀ (t : ℕ), ↑t ≥ C * ↑n ^ 3 → |↑(paperCount n (4 * t)) / paperAsymptoticCount n t - (1 - ↑(n.choose 3) / (8 * ↑t))| ≤ K * ↑n ^ 2 / ↑t + K * (↑n ^ (5 / 2) / ↑t ^ (3 / 2)) + K * ↑n ^ 6 / ↑t ^ 2 + K * Real.exp (-(c * ↑n ^ 2))

Count theorem matching the main asymptotic theorem in the arXiv paper.

This is the main paper asymptotic for the number N_{n,4t} of n × 4t partial Hadamard matrices.

theorem cor_uniform (ε : ℝ) : 0 < ε → ∃ (K : ℝ), 0 < K ∧ ∀ (n : ℕ), 2 ≤ n → ∀ (t : ℕ), ↑t ≥ K * ↑n ^ 3 → |↑(paperCount n (4 * t)) / paperAsymptoticCount n t - 1| < ε

Lean wrapper for the uniform corollary in the arXiv paper.

For sufficiently large t ≥ K n^3, the normalized paper count ratio N_{n,4t} / A_{n,4t} is uniformly close to 1.