Partial Hadamard matrices in the cubic regime — Blueprint

1 Overview

This blueprint maps the Lean formalization of arXiv:2603.30013, which gives a first-order asymptotic expansion for partial Hadamard matrices in the cubic regime \(t\ge C_0 n^3\). Every labeled result in the paper is formalized without sorry or internal axiom.

Navigation

  • Main results: Theorem 26 and Corollary 27 (Chapter 6).

  • Setup: Lattice structure, decompositions, pointwise bounds, fixed-\(n\) asymptotics, and analytic tools (Chapter 2).

  • Core analysis: Cumulants, quartic bounds, log-expansion, small-ball decay, cubic phase bound, and the primary estimate (Chapter 4).

  • Weak comparison: Lindeberg replacement and Gaussian comparison (Chapter 3).

  • Far shell and residual: Far-shell contraction, far-shell integrals, and the residual estimate (Chapter 5).

  • Module guide: File-by-file map of the Lean source (Chapter 7).

  • Dependency graph.