2.2 Results from de Launey–Levin

Lemma 1 Cosine-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\} })\).

Lemma 2 Lattice 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.

Proposition 3 Primary-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 . \]

Lemma 4 Residual 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.

Proof ▶

The translates \(\mathcal{B}_{\pi /4}(\lambda )\), \(\lambda \in \Lambda _0\), tile \(\mathbb {T}^d\). Even cells centered at \(\lambda \in \Lambda \) contribute to \(R_\delta ^{\mathrm{even}}\); odd cells centered at \(\lambda \in \Lambda _0\setminus \Lambda \) contribute to \(R_\delta ^{\mathrm{odd}}\).

Lemma 5 Odd-cell bound

✓

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

Proof ▶

Since \(\gamma \) lies in a quarter-box centered at \(\lambda \in \Lambda _0\setminus \Lambda \), some vertex \(k\) has odd degree in \(G_{\lambda ^{(2)}}\), so \(\prod _{i\ne k}\cos (2\gamma _{\{ i,k\} })\le 0\), and the cosine-product bound (Lemma 1) gives \(|\psi (\gamma )|^2\le 1/2\).

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

✓

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

Proof ▶

\(\operatorname {Re}\psi (\lambda )=\mathbb {E}[\cos X_\lambda ]\ge 1-\frac12 s(\lambda )\ge 3/4\).