Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Corollary 24Far-shell integrals

Let \(E_r(n,t):=q_{\mathrm{sm}}^{4t}+q_{\mathrm{big}}^{4t}+e^{-a_r t n^{-2/3}}\). Then for every \(\delta \in (0,\pi /4)\),

\[ \begin{aligned} K_n\int _{\mathcal{B}_\delta \setminus \mathcal{D}_r}|\psi (\lambda )|^{4t}\, d\lambda & \le 2^{-n+1}E_r(n,t),\\ (2\pi )^{-d}\sum _{\lambda \in \Lambda } \int _{\lambda +(\mathcal{B}_{\pi /4}\setminus \mathcal{D}_r)}|\psi (\gamma )|^{4t}\, d\gamma & \le 2^{-n+1}E_r(n,t). \end{aligned} \]

Both are \(o(\hat A_{n,4t})\) as \(n\to \infty \) with \(t/(n^{8/3}\log t)\to \infty \).

LaTeX Lean

Corollary 27Uniform counting

For every \(\varepsilon {\gt}0\) there exists \(K{\gt}0\) such that

\[ \left|\frac{N_{n,4t}}{A_{n,4t}}-1\right|{\lt}\varepsilon \qquad \text{for all } n\ge 2 \text{ and } t\ge Kn^3. \]

LaTeX Lean

Corollary 13Gaussian comparison

Let \(\psi _G\) be the characteristic function obtained by replacing the Rademacher entries \(\xi _i\) with i.i.d. standard Gaussians \(g_i\). For each row \(k\in [n]\), define the row influence \(I_k(\lambda ):=\sum _{i\ne k}\lambda _{\{ i,k\} }^2\), and set \(J(\lambda ):=\sum _{k=1}^n I_k(\lambda )^{3/2}\). Then

\[ |\psi (\lambda )-\psi _G(\lambda )|\le \tfrac 32 J(\lambda ) \qquad \text{for every }\lambda \in \mathbb {R}^d. \]

LaTeX Lean

Lemma 7Fixed-\(n\) asymptotics

For every fixed integer \(n\ge 2\), \(N_{n,4t}=[1+o_{t\to \infty }(1)]\, A_{n,4t}\) as \(t\to \infty \).

LaTeX Lean

Lemma 2Lattice structure

The formalization proves the following (as private lemmas in HadamardCn3TorusCount.lean):

Multiplicativity: \(\psi (\lambda +\gamma )=\psi (\lambda )\psi (\gamma )\) for \(\lambda \in \Lambda \), \(\gamma \in \mathcal{B}_{\pi /4}\) (psi_translate_lambdaReal).
Disjoint boxes: the translates \(\mathcal{B}_\delta (\lambda )\), \(\lambda \in \Lambda \), are pairwise disjoint for \(\delta {\lt}\pi /4\) (translated_edgeBoxes_disjoint).
Cardinality: \(|\Lambda |=2^{2d-n+1}\) and \(\psi (\lambda )^{4t}=1\) for \(\lambda \in \Lambda \) (card_lambdaShifts_eq_pow_of_two_le, exp_phase_lambdaReal_false_pow_four_mul).
Even-degree characterization: \(\lambda \in \Lambda \) iff every vertex of \(G_{\lambda ^{(2)}}\) has even degree (parityEvenBool_iff_incidence_zero).

These are private because they are only used internally by the torus counting machinery.

LaTeX

Lemma 1Cosine-product bound

For every \(\gamma \in [-\pi ,\pi ]^d\) and every \(k\in \{ 1,\dots ,n\} \), \(|\psi (\gamma )|^2\le \frac12+\frac12\prod _{i\ne k}\cos (2\gamma _{\{ i,k\} })\).

LaTeX Lean

Lemma 21Cubic phase bound

For all \(d,t\ge 1\),

\[ \operatorname {Re}\int _{\mathcal{D}_\mathrm {core}}e^{-2t\| \lambda \| ^2}e^{-4itT(\lambda )}\, d\lambda \ge \bigl[1-O(n^3/t)\bigr]G_{\mathrm{core}}(d,t). \]

LaTeX Lean

Lemma 10Gaussian quadratic integral

Let \(A\) be a complex symmetric \(m\times m\) matrix whose real part is positive definite. Then \(\int _{\mathbb {R}^m}e^{-x^\top A x}\, dx=\pi ^{m/2}\det (A)^{-1/2}\). In particular, if \(g\sim N(0,I_m)\) and \(M\) is real symmetric, \(|\mathbb {E}[e^{ig^\top Mg/2}]|=\det (I+M^2)^{-1/4}\).

LaTeX Lean

Lemma 9Gaussian radial moments

For every integer \(m\ge 0\) there is \(C_m{\gt}0\) such that \(\int _{\mathbb {R}^d}\| \lambda \| ^{2m}e^{-2t\| \lambda \| ^2}\, d\lambda \le C_m(d/t)^m F(d,t)\) for all \(d,t\ge 1\).

LaTeX Lean

Lemma 8Hypercontractive inequality

Let \(H\) be a polynomial of degree at most \(q\) in either independent Rademacher signs or independent centered Gaussians. Then for every \(p\ge 2\), \(\| H\| _{L^p}\le (p-1)^{q/2}\| H\| _{L^2}\).

LaTeX Lean

Lemma 11Core Gaussian mass

There exists an absolute constant \(c_*{\gt}0\) such that \(G_{\mathrm{core}}(d,t)\ge (1-e^{-c_*d})F(d,t)\).

LaTeX Lean

Lemma 5Odd-cell bound

If \(\gamma \in R_\delta ^{\mathrm{odd}}\), then \(|\psi (\gamma )|^2\le \tfrac 12\).

LaTeX Lean

Lemma 15Fourth cumulant

\(Q(\lambda ) =-\frac{1}{12}\sum _e\lambda _e^4+\frac18\mathcal{C}_4(\lambda )\), where \(\mathcal{C}_4(\lambda )=\sum _{\text{ordered 4-cycles}}\lambda _{i_1 i_2}\lambda _{i_2 i_3}\lambda _{i_3 i_4}\lambda _{i_4 i_1}\).

LaTeX Lean

Lemma 16Peeling identity

Let \(A\) be a symmetric zero-diagonal \(n\times n\) matrix, \(B\) the \((n{-}1)\times (n{-}1)\) submatrix deleting row/column \(n\), \(x\in \mathbb {R}^{n-1}\) the last column, and \(M(B)=B^2-\operatorname {diag}(B^2)\). Then

\[ Q_n(A)=Q_{n-1}(B)+\tfrac 12 x^\top M(B)x-\tfrac {1}{12}\sum _{a=1}^{n-1}x_a^4. \]

LaTeX Lean

Lemma 18Quintic bound

There is \(C_3'{\gt}0\) such that

\[ \int _{\mathcal{D}_\mathrm {core}}P(\lambda )^2 e^{-2t\| \lambda \| ^2}\, d\lambda \le C_3'\frac{n^5}{t^5}G_{\mathrm{core}}(d,t). \]

LaTeX Lean

Lemma 6Positivity of \(\operatorname {Re}\psi \)

If \(s(\lambda )\le 1/2\), then \(\operatorname {Re}\psi (\lambda )\in [3/4,1]\).

LaTeX Lean

Lemma 4Residual decomposition

For \(0{\lt}\delta {\lt}\pi /4\),

\[ R_\delta = R_\delta ^{\mathrm{even}} \cup R_\delta ^{\mathrm{odd}}, \qquad R_\delta ^{\mathrm{even}} = \bigcup _{\lambda \in \Lambda }\bigl(\lambda +[\mathcal{B}_{\pi /4}\setminus \mathcal{B}_\delta ]\bigr), \qquad R_\delta ^{\mathrm{odd}} = R_\delta \setminus R_\delta ^{\mathrm{even}}, \]

and the sets in the union are disjoint.

LaTeX Lean

Lemma 19Log-expansion

There are \(c_2,C_2{\gt}0\) such that whenever \(s(\lambda )\le c_2\),

\[ \log \psi (\lambda ) =-\tfrac 12 s(\lambda )-iT(\lambda )+Q(\lambda )+iP(\lambda )+E_6(\lambda ) \]

with \(|E_6(\lambda )|\le C_2 s(\lambda )^3\).

LaTeX Lean

Lemma 20Small-ball decay

There exists \(r_0\in (0,\pi /4)\) such that \(|\psi (\lambda )|^{4t}\le e^{-3t\| \lambda \| ^2/2}\) for every \(t\ge 1\) and \(\lambda \in \mathcal{D}_{r_0}\).

LaTeX Lean

Lemma 14Triangle formula

For every \(\lambda \in \mathbb {R}^d\), \(T(\lambda )=\sum _{1\le i{\lt}j{\lt}k\le n}\lambda _{ij}\lambda _{ik}\lambda _{jk}\).

LaTeX Lean

Lemma 12Lindeberg comparison

Let \(f:[n]^2\to \mathbb {R}\) be symmetric with \(f(i,i)=0\), and define

\[ Q_f(z):=\sum _{1\le i,j\le n}f(i,j)z_i z_j, \qquad \mathrm{Inf}_m(f):=\sum _{j=1}^n f(m,j)^2. \]

If \(X_1,\dots ,X_n\) are independent Rademacher signs, \(G_1,\dots ,G_n\) are i.i.d. \(N(0,1)\), and \(\varphi :\mathbb {R}\to \mathbb {R}\) is \(C^3\), then

\[ \left|\mathbb {E}[\varphi (Q_f(X))]-\mathbb {E}[\varphi (Q_f(G))]\right| \le 6\| \varphi '''\| _\infty \sum _{m=1}^n \mathrm{Inf}_m(f)^{3/2}. \]

LaTeX Lean

Proposition 23Far-shell contraction

Set \(\eta _r:=\frac{1}{3}[1-(1+2r^2)^{-1/4}]\) and \(I_{\max }(\lambda ):=\max _k I_k(\lambda )\). There exist \(q_{\mathrm{sm}},q_{\mathrm{big}}\in (0,1)\) and \(a_r{\gt}0\) such that for all \(n\ge 2\) and \(t\ge 1\) the far shell decomposes as

\[ \begin{aligned} \mathcal F_{\mathrm{sm}} & :=\{ \lambda \in \mathcal{B}_{\pi /4}\setminus \mathcal{D}_r:J(\lambda )\le \eta _r\} ,\\ \mathcal F_{\mathrm{big}} & :=\{ \lambda \in \mathcal{B}_{\pi /4}\setminus \mathcal{D}_r:J(\lambda ){\gt}\eta _r,\; I_{\max }\ge 1\} ,\\ \mathcal F_{\mathrm{mid}} & :=\{ \lambda \in \mathcal{B}_{\pi /4}\setminus \mathcal{D}_r:J(\lambda ){\gt}\eta _r,\; I_{\max }{\lt}1\} , \end{aligned} \]

and

\[ |\psi (\lambda )|^{4t}\le \begin{cases} q_{\mathrm{sm}}^{4t} & \lambda \in \mathcal F_{\mathrm{sm}},\\ q_{\mathrm{big}}^{4t} & \lambda \in \mathcal F_{\mathrm{big}},\\ \exp (-a_r t n^{-2/3}) & \lambda \in \mathcal F_{\mathrm{mid}}. \end{cases} \]

LaTeX Lean

Proposition 22Primary estimate

Set \(K_n:=2^{2d-n+1}(2\pi )^{-d}\). For all sufficiently large \(n\) and \(t\ge C_0 n^3\),

\[ K_n\operatorname {Re}\int _{\mathcal{D}_\mathrm {core}}\psi (\lambda )^{4t}\, d\lambda =\left(1-\frac{\binom {n}{3}}{8t} +O\! \left(\frac{n^2}{t}+\frac{n^{5/2}}{t^{3/2}}+\frac{n^6}{t^2} +e^{-cd}\right)\right)\hat A_{n,4t}. \]

LaTeX Lean

Proposition 3Primary-secondary decomposition

For every \(t\ge 1\) and every \(0{\lt}\delta {\lt}\pi /4\),

\[ \mathbb {P}(S_{4t}=0) = 2^{2d-n+1}(2\pi )^{-d}\int _{\mathcal{B}_\delta }\psi (\lambda )^{4t}\, d\lambda +(2\pi )^{-d}\int _{R_\delta }\psi (\gamma )^{4t}\, d\gamma . \]

LaTeX Lean

Proposition 17Quartic bounds

There exist \(c_1,C_1{\gt}0\) such that if \(d/t\le c_1\) and \(nd^2/t^2\le c_1\), then

\[ \int _{\mathcal{D}_\mathrm {core}}|e^{4tQ(\lambda )}|^2 e^{-2t\| \lambda \| ^2}\, d\lambda \le C_1G_{\mathrm{core}}(d,t), \]

and

\[ \int _{\mathcal{D}_\mathrm {core}}|e^{4tQ(\lambda )}-1|^2 e^{-2t\| \lambda \| ^2}\, d\lambda \le C_1\frac{d^2}{t^2}G_{\mathrm{core}}(d,t). \]

LaTeX Lean

Proposition 25Residual estimate

Set \(\delta ^2=2d/t\) and \(K_n:=2^{2d-n+1}(2\pi )^{-d}\). Then

\[ \begin{aligned} K_n\int _{\mathcal{B}_\delta \setminus \mathcal{D}_\mathrm {core}}|\psi (\lambda )|^{4t}\, d\lambda & = o(\hat A_{n,4t}),\\ (2\pi )^{-d}\left|\int _{R_\delta }\psi (\gamma )^{4t}\, d\gamma \right| & = o(\hat A_{n,4t}), \end{aligned} \]

as \(n\to \infty \) with \(t/(n^{8/3}\log t)\to \infty \). For \(t\ge C_0 n^3\) and all sufficiently large \(n\), both bounds are at most \(Ce^{-cn^2}\hat A_{n,4t}\).

LaTeX Lean

Theorem 26Main asymptotic count

There exist \(C_0,c{\gt}0\) such that for all sufficiently large \(n\) and \(t\ge C_0 n^3\),

\[ \frac{N_{n,4t}}{A_{n,4t}} =1-\frac{\binom {n}{3}}{8t} +O\! \left(\frac{n^2}{t}+\frac{n^{5/2}}{t^{3/2}} +\frac{n^6}{t^2}+e^{-cn^2}\right). \]

LaTeX Lean