7 Module guide
File-by-file map of the Lean formalization.
- HadamardCn3Defs
Core definitions: \(d=\binom {n}{2}\), edge type, \(\psi \), \(\| \lambda \| ^2\), Gaussian scale \(\hat A_{n,4t}\), count scale \(A_{n,4t}\), normalized count \(N_{n,4t}/2^{4nt}\), matrix structure.
- HadamardCn3TorusCount
Torus counting infrastructure: Fourier inversion, prefactors, combinatorial cycle formulas, hypercontractive bounds, Gaussian radial moments, quartic and quintic cumulant estimates.
- HadamardCn3Moments
Moment bounds: fourth, sixth, and eighth moment estimates for polynomial corrections to the Gaussian integrand.
- HadamardCn3MOO
Mossel–O’Donnell–Oleszkiewicz kernel infrastructure: row influence, kernel influence, the three-halves influence sum \(J(\lambda )\).
- HadamardCn3WeakInvariance
Lindeberg replacement proof: hybrid vectors, Taylor expansion, moment matching, and the weak comparison theorem (Lemma 12 and Corollary 13).
- HadamardCn3QuarticFiber
Quartic fiber analysis: peeling identity, ordered cycle formula, and pointwise quartic bounds.
- HadamardCn3LocalGapBridge
Bridge estimates: log-expansion, small-ball decay, cubic phase bound, core-to-corrected-to-quartic-to-cubic bridge chain, primary annulus and far-shell integral bounds.
- HadamardCn3LocalGapResidual
Residual estimates: primary core contribution, shell transport, annulus bound, far-shell bound, and the quantitative residual theorem (Proposition 25).
- HadamardCn3LocalGapFixedN
Fixed-\(n\) analysis: shrinking-box infrastructure with \(\delta _t=t^{-2/5}\), fixed-\(n\) normalized-count and count asymptotics (Lemma 7).
- HadamardCn3Asymptotics
Intermediate bridge: primary-box estimate on the Gaussian scale, normalized-count asymptotic combining primary and residual.
- HadamardCn3ShortMain
Paper-facing theorems: Theorem 26 and Corollary 27, with the count normalization.
- HadamardCn3ResidualBase
Residual base estimates: supporting lemmas for the residual route.