Dependencies

A family of positive integers is lacunary if every dyadic window \([X, 2X]\) contains \(O(1)\) of its members.

For a marked Hepp tree: injections \((z_{\mathfrak l})\colon \mathcal{L} \to \mathbb {Z}^4_M\) with \(\lvert z_{\mathfrak l} - z_{{\mathfrak l}'}\rvert \ge \tfrac 12 N_{{\mathfrak l}\vee {\mathfrak l}'}\) and the linked-children condition (b); realizability \(Z \leftrightarrow (\mathcal{T}, N)\); the multiset/multiplicity variants.

\(\mathcal{J}_{2q,\sigma }\), \(\mathcal{C}_{2q,\sigma }\), \(\mathcal{C}_{2q}\), and \(\mathcal{C}_\varepsilon = \sum _{q\le A}\mathcal{C}_{2q}\); the primitive-with-insertions structure of full pairings.

Functions on \(\mathbb {T}^4\) (resp. \(\mathbb {R}^4\)) invariant under coordinate permutations and per-coordinate sign flips (hyperoctahedral \(B_4\)). The formalization uses this single-slot interpretation.

A Hepp tree is a plane rooted tree in which every internal node has at least two children (carrier PlaneTree; leaves are identified by their position paths), together with, as separate data: a marking \(N\colon \) branching nodes \(\to 2^{\mathbb {N}}\), strictly increasing toward the root, and multiplicities \(m\colon \) leaves \(\to \mathbb {N}_{\ge 2}\). Derived notation: \(\mathcal{B}\), \(\mathcal{L}\), \(\gamma _{\mathfrak n}\), subtrees, least common ancestors. Automorphisms are order-forgetting: recursive child permutations preserving subtree shape (and marks, for \(\mathrm{Aut}(\mathcal{T},N)\)); concretely accessed through recursive canonicalization. The finite group \(\mathrm{Aut}(\mathcal{T})\), its action on leaves and markings, and the stabilizer description of \(\mathrm{Aut}(\mathcal{T},N)\) are part of the checked definition layer.

\(\mathcal{I}_m = \sum _\kappa \mathcal{I}_{m,\kappa }\): the deterministic profile kernels integrated against chaos projections of \(\prod _{i\in S}\xi _\varepsilon (x_i)\).

For a linearly ordered finite index set: subintervals \([a,b]\); a subinterval \(B\) is fully paired under \(\kappa \) if \(\kappa \) induces a full pairing on \(B\); \(\kappa \) is primitive if no proper subinterval is fully paired. The L0 API also provides: the induced pairing after removing a fully paired subinterval (paper Def. 3.1(2a)), the smallest-leftmost fully paired subinterval selector with its uniqueness lemma, and enumeration finsets for fixed index sets (needs of 44 and §4.1).

For each \((m,\kappa )\), the deterministic factor of the chaos expansion: products of \(G\)-factors along the chain and \(\eta _\varepsilon \)-factors along the pairs, with the single-index variables as free arguments; generalized inputs \([G_0,\dots ,G_m]\).

Leaf types, \(\gamma ^2_{\mathfrak n}\), \(\gamma ^\infty _{\mathfrak n}\), and the power-counting identity (5.31).

Words are maps \(w\colon \mathrm{Fin}\, m \to \mathcal{L}\) with prescribed fiber sizes; \(\mathrm{wordSum}\) sums a functional over them, and the definitional ledger is \(\mathrm{paperSum} := \big(\prod _{\mathfrak l} m_{\mathfrak l}!\big) \cdot \mathrm{wordSum}\). Paper-facing statements use \(\mathrm{paperSum}\) on the left with the paper’s right-hand sides verbatim; proofs manipulate \(\mathrm{wordSum}\). Includes the no-adjacent-equal-letters and primitivity predicates on words, and the labeled-arrangement fiber-count lemma (\(\# \{ \text{labeled arrangements inducing } w\} = \prod _{\mathfrak l} m_{\mathfrak l}!\)).

The four-point kernel \(H(x_1,y_1,x_2,y_2) = \int G(x_1-z)G(y_1-z)G(x_2-z)G(y_2-z)\, \mathrm{d}z\); the centered Gaussian law on the realification \(\mathbb {R}^{2s}\) of the chosen modes, with the full real covariance determined by \(\frac{2\pi ^2}{2\pi ^2-\lambda ^2}\widehat H\) on mode pairs (conjugate modes supplying the pseudo-covariance); positive semidefiniteness and existence for \(\lambda ^2 {\lt} 2\pi ^2\); junk law otherwise.

A partial pairing \(\kappa \) of a finite index set \(A\) is a partition of a subset \(P \subseteq A\) into disjoint two-element subsets (pairs); \(S = A \setminus P\) is the set of single indices. If \(S = \varnothing \), \(\kappa \) is a full pairing.

Random \(\mathcal{RI}_{m,\kappa }\), \(\mathcal{P}_m\), \(\mathcal{P}_\varepsilon = \sum _{m\le A}\mathcal{P}_m\). Operator realization: \(K_\varepsilon := G \circ M_\varepsilon \) with \(M_\varepsilon \) multiplication by \(\lambda _\varepsilon \xi _\varepsilon - \mathcal{C}_\varepsilon \); invertibility predicate \(:=\) invertibility of \(1 - K_\varepsilon \) in \(\mathcal{B}(L^2)\); primary mode objects \(\mathrm{modeCoeffH}(\alpha ,\beta ) = \big\langle e_{-\alpha }, \big((1-K_\varepsilon )^{-1}G - G\big)e_\beta \big\rangle \) on the invertibility event and \(0\) off it; the conditioned HS-difference lemma \((1-K_\varepsilon )^{-1}G - G = (1-K_\varepsilon )^{-1}\, G M_\varepsilon G\) with the \((1+\log )\)-weighted Hilbert–Schmidt bound.

\(\mathcal{RI}\) at the deterministic level: repeatedly remove the smallest-leftmost fully paired subinterval, via \(J\) and \(\widetilde G\) ((3.3)–(3.5)).

The sufficient parent-function injection estimate \(\sum _{\mathcal H}\prod _i (1 + w_i)^{d(i)-1} \le \big(q + \sum _i w_i\big)^{q-1}\) used in Step 5 of the proof of 12. This replaces the paper’s exact weighted Cayley identity by the weaker conclusion actually needed in (5.24)–(5.25), obtained from an injection into parent functions.

The minimal API for Wiener-chaos projections of Gaussian polynomials (orthogonality between orders; enough for (2.4) and the Wick reduction of 46; Prop. 3.6 being external, no product formula beyond what 44 needs).

Convergence of all joint moments to those of a Gaussian vector implies convergence in distribution (moment determinacy of Gaussians; finite-dimensional). Realized in the fixed-truncation form consumed by the assembly.

\(G := \int _0^\infty e^{-t}\, \Theta (t,\cdot )\, \mathrm{d}t\) with \(\Theta \) the periodized Gaussian (Bessel-potential representation; a Fourier tsum is ill-defined since \(\langle k\rangle ^{-2}\notin \ell ^1\cup \ell ^2\) and \(G \notin L^2\)). Lemmas: \(\widehat G(k) = \langle k\rangle ^{-2}\); \(G \in \mathcal{E}\); \(\lvert \nabla ^k G(z)\rvert \lesssim \lvert z\rvert ^{-2-k}\) (\(k \le 2\)); the improved near-diagonal bound for \(G - \frac{1}{4\pi ^2\lvert z\rvert ^2}\).

For a finite jointly-Gaussian centered family, \(\mathbb {E}\big[\prod _j X_j\big] = \sum _{\kappa \text{ full pairing}} \prod _{\{ i,j\} \in \kappa }\mathbb {E}[X_iX_j]\), proved by a self-contained induction.

Kernels vs. \(\mathcal{B}(L^2(\mathbb {T}^4))\): operator norms from Plancherel double sums (no named Hilbert–Schmidt API assumed); Neumann-series inversion.

The canonical probability space of independent standard real Gaussians, two per \(\{ \pm k\} \)-orbit and one for the zero mode; the assembled complex coefficients \(g_k\) with \(\mathbb {E}[g_k g_l] = \mathbf{1}_{k=-l}\), \(\mathbb {E}[g_k \overline{g_l}] = \mathbf{1}_{k=l}\); the mollified noise \(\xi _\varepsilon = (2\pi )^{-2}\sum _k \widehat\rho (\varepsilon k)\, g_k e_k\) (the Lebesgue/probability-Haar half-density from the normalization ledger), a.s. \(C^\infty \), with a single probability-one event working simultaneously for every countable scale family; the covariance identity \(\mathbb {E}[\xi _\varepsilon (x)\xi _\varepsilon (y)] = \eta _\varepsilon (x-y)\), \(\eta = \rho * \rho \).

Chain convolution bounds for \(\lvert z\rvert ^{-2}\)-kernels on \(\mathbb {T}^4\); the estimates (5.3)–(5.4); \(\eta _\varepsilon \)-support handling.

Characters \(e_k\), kernel coefficients (3.23) \(\widehat K(\alpha ,\beta ) = \langle e_{-\alpha }, K e_\beta \rangle \), Plancherel on the product torus, multiplier calculus, and the normalization ledger dictionary.

Filter-indexed convergence-in-distribution lemmas for realified mode vectors (mathlib’s sequence-indexed statements transported to the \(\varepsilon \)-filter); restriction to good events of probability tending to one.

For every \(\alpha {\gt} 1\) there is \(\beta = \beta (\alpha )\) with \(\binom {m+n}{m} \le \alpha ^m \beta ^n\); the multinomial analogue (paper (5.50)); and the lacunary version (paper (5.51)) with a uniform \(C^{n_1+\dots +n_r}\) bound.

For \(\theta {\gt} 0\) and \(m \le n\): \(\sum _{1\le z_1,\dots ,z_m\le n}\prod _{j=1}^{m-1} \min \big(1, 2^{-\theta (z_j - z_{j+1})}\big) \le C(\theta )^n\); the dyadic version (paper (5.56)); and the variants skipping at most 100 factors.

For \(A, B \subseteq \mathbb {Z}^4\) with separations \(M, N\) and \(P = \lvert A\rvert M^4\), \(Q = \lvert B\rvert N^4\): the bilinear bound (5.58) with right-hand side \(\lvert A\rvert ^{1/2}M^{-2}\, \lvert B\rvert ^{1/2}N^{-2} \min \big(1, (Q/P)^{1/4}\big)\), by dyadic shell counting.

The number of plane rooted trees with \(r\) leaves in which every internal node has at least two children is at most \(C^r\) for an explicit absolute constant \(C\). Such trees have at most \(2r-1\) vertices; the balanced-parentheses serialization injects them into Dyck-type words of bounded length, giving an explicit \(C\).

Every finite \(Z \subseteq \mathbb {Z}^4_M\) is realized by some marked Hepp tree with \(1 {\lt} N_{\mathfrak n} \lesssim M\) (greedy scale construction); every paired vector \((y_j)\) is realized in the multiplicity sense with even multiplicities.

The explicit formula (3.6): difference factors \(G(x_{r_i} - x_{r_i+1}) - G(x_{\ell _i} - x_{r_i+1})\) at the removed endpoints.

The explicit formula (3.12).

\(\lambda _\varepsilon \xi _\varepsilon \circ \mathcal{P}_{m-1} = (1-\Delta )\mathcal{P}_m + \sum _{1\le q\le m/2} \mathcal{C}_{2q}\mathcal{P}_{m-2q}\) and its mirror (3.17), as Fourier-multiplier identities of random kernels; proof by the three-case analysis of pairings of the new index.

\(\lvert \mathcal{C}_{2q}\rvert \le \varepsilon ^{-2} \lvert \log \varepsilon \rvert ^{-1}(C\lambda )^{2q}\) for \(1 \le q \le A\).

\(\mathbb {E}\lvert \widehat{\mathcal{P}_m}(\alpha ,\beta )\rvert ^2 \le \lambda _\varepsilon ^2\, C(C\lambda )^{2m-2}\min \big(1, \varepsilon ^{-8}\langle \alpha \rangle ^{-4}\langle \beta \rangle ^{-4} \langle \varepsilon ^2(\alpha +\beta )\rangle ^{-8}\big)\): the Wick reduction to 34.

The deterministic pairing-sum bound underlying (3.24), including the decay factors \(\langle \alpha \rangle ^{-4}\langle \beta \rangle ^{-4} \langle \varepsilon ^2(\alpha +\beta )\rangle ^{-8}\).

Quoted by the paper from Gabriel–Rosati (arXiv:2602.22509, Props. 3.9 and 3.12); stated in Lean in full and taken as a hypothesis of the main theorem. Literal quantifier form (PAPER_MAP.md remark 6): for every \(B, r\) there exist \(\mathfrak {X}_B\) with \(\lvert \mathfrak {X}_B(m_1,m_2)\rvert \le C(C\lambda )^{m_1+m_2-2}\) for positive orders and (3.28), summed over \(m_1,m_2\ge 1\), with value \((\lambda /(\sqrt{2}\, \pi ))^{m-2}\) for even \(m\le B\) and \(0\) for odd \(m\le B\), such that for every positive-order mode family, eventually in \(\varepsilon \), (3.26)–(3.27) hold uniformly over orders \(m_j \le B\), with the literal (3.26) error \(O(\lambda _\varepsilon ^r/\lvert \log \varepsilon \rvert )\). The public Prop36Family interface is precisely the hypothesis consumed by main_conditional. The interface also exposes the measurability of each coefficient and integrability of every displayed finite product, implicit in the paper’s use of these expressions as moments.

The bounds (4.3) and (4.4) on \(\mathcal{J}_{2n,\mathrm{prim}}\), with and without the \(\varepsilon ^2 + \max \lvert x_i - x_j\rvert ^2\) insertion, for \(1 \le n \lesssim \lvert \log \varepsilon \rvert \).

The estimate (5.39) for word sums with a skipped set \(O\) (\(\mathrm{paperSum}\) normalization; no primitivity assumed): scale classification \(\sigma _1,\sigma _2,\sigma _3\), outer \(\boldsymbol {X}\)-sum (5.76)–(5.86), inner \(\pi \)-sum (5.87)–(5.98) via the local inequalities (5.90)–(5.92). Formalization makes explicit the inclusive-ancestor constant in (5.69) and uses the exponent \(2(m_{\mathfrak l}-2)\) in both simple-leaf products of (5.83); see docs/PAPER_NOTES.md.

The orbit-stabilizer lower bound (5.12) for the number of markings realizing a given embedding, and the embedding-counting upper bounds (5.13)–(5.14) with automorphism factors \(\lvert \mathrm{Aut}(\mathcal{T})\rvert / \lvert \mathrm{Aut}(\mathcal{T},N)\rvert \) and \(\prod _{\mathfrak n} N_{\mathfrak n}^{4(\gamma _{\mathfrak n}-1)}\) (and the \(\langle z_0 - z_1\rangle ^{-4}\)-refined variant). Six-step proof as in the paper’s §5.3.

The estimate (5.15): \(\mathrm{paperSum}\) of the inverse-square chain weights is bounded by \(C^n \sum _{W\subseteq \mathcal{B}\setminus \{ \mathfrak r\} } (n - \lvert W\rvert )!\, \prod (m_{\mathfrak l}!)^{1/2}\cdots \) — the log-loss/factorial-gain balance. Derived from 18 by merging adjacent equal copies ((5.34)–(5.37)); the constants \(C_0, D\) are discharged here.

The generalized estimate (5.33) with compound leaves under (5.32), constants \(C_0 {\gt} 1000\), \(D = e^{C_0^{10}}\). Proof by induction on the tree: choose the lowest branching node satisfying (5.40); collapse its subtree to a compound leaf via the word-level collapse equivalence \(\pi \leftrightarrow (\pi _1, O, \pi _2)\); comparability (5.41); factor bookkeeping (5.42)–(5.48), with the \(((s+1)!)^{-1}\) of (5.45)(i) supplied by the ledger 13.

\(\mathcal{L}_\varepsilon \mathcal{P}_\varepsilon = 1 + \mathcal{R}_\varepsilon \) in multiplier form, with the explicit error kernels \(\mathcal{R}_\varepsilon , \mathcal{R}'_\varepsilon \).

\(\mathbb {E}\| \mathcal{P}_m\| ^2_{L^2\to L^2}\) via Plancherel double sums ((3.30)–(3.31)); \(\mathbb {E}\| \mathcal{P}_\varepsilon \| \le \varepsilon ^{-12}\), \(\mathbb {E}(\| \mathcal{R}_\varepsilon \| + \| \mathcal{R}'_\varepsilon \| ) \le \varepsilon ^{30}\); the Chebyshev good event \(Z_\varepsilon ^c\); Neumann inversion and \(\| \mathcal{L}_\varepsilon ^{-1} - \mathcal{P}_\varepsilon \| _{L^2\to L^2} \le \varepsilon ^{12}\) (3.33).

Truncation \(\mathcal{Q}_{B,\varepsilon }\); joint moments converge to Gaussian moments ((3.36)–(3.37)) with the mode family closed under negation; invoking Proposition 3.6 at order bound \(2B\) makes (3.28) determine the aggregate pair covariance of \(\mathcal Q_{B,\varepsilon }\) without a cross-truncation choice; the \(B \to \infty \) geometric summation \(\mathfrak {X}_B \to \frac{2\pi ^2}{2\pi ^2-\lambda ^2}\) ((3.38)–(3.39)).

On the good event, replacement of \(\mathcal{H}_\varepsilon \) by the truncated \(\mathcal{Q}_\varepsilon \) for any fixed finite mode family (mode functionals are controlled by operator norms; \(\mathbb {P}(Z_\varepsilon ) \to 0\)). No tightness is needed for the finite-mode target.

Moments of \(\prod _j \xi _\varepsilon (x_j)\) as sums over full pairings of \(\eta _\varepsilon \)-factors; the chaos decomposition of products with partial pairings and \(\mathrm{Proj}_{\lvert S\rvert }\).

Dyck-word bookkeeping of nested fully paired subintervals; iterative reduction integrating out innermost intervals; Taylor expansion with \(\mathcal{E}\)-symmetry killing the linear term (4.9); the three-case integral bounds (4.10)–(4.12).

The same reduction machine plus oscillation in \((x,y,z,w)\) for the decay factors ((4.16)–(4.20)). The formal proof follows the paper’s two endpoint cases and retains the truncation \(A = \lfloor |\log \varepsilon |\rfloor \) until the final numerical assembly.

In Step 4(B), the paper obtains the total-frequency gain by finding a first large/high slot among the at most \(A\) composition factors. The Lean proof keeps the complete signed open series through the removals, translates the common surviving left half, extracts its Fourier coefficient, selects a nonzero coordinate of \(\alpha +\beta \), and integrates by parts eight times. The only norm is taken after this whole-family Fourier extraction. This is an alternative Lean proof of the same required \(\langle \varepsilon ^2(\alpha +\beta )\rangle ^{-8}\) decay conclusion, not the paper’s literal first-large/high-slot proof.

Declaration-by-declaration links are recorded in PAPER_TO_LEAN.md, Step 4(B).

The (5.1)-form lattice estimate from 12 and 19: geometric \((N_{\mathfrak n})\)-summation (5.16)–(5.17), the endpoint refinement \(\min (\lvert W\rvert + 1, n-2)\), and the elementary inequality \((n-s)!\, \lvert \log \varepsilon \rvert ^{\min (s+1,n-2)} \le C^n\lvert \log \varepsilon \rvert ^{n-2}\). Consumed by 26 through the discretization interface 25.

Reduction of 26 to the lattice counting bound (5.5): choice of \(\mathcal{A}\), discretization \(y_j = \lfloor \varepsilon ^{-1}x_j\rfloor \), and the singular-integral bounds (5.2)–(5.4).

The master reduction of the counting sum (5.5): fix the tree (\(C^n\) choices by 3), the multiplicities and the ordering data; the symmetry-factor denominator; and the word-sum bound (5.10) in the normalization of 13, with \(\mathrm{pairedWordSum}\) on the left and \(\big(\prod _{\mathfrak l}(m_{\mathfrak l}/2)!/m_{\mathfrak l}!\big) \mathrm{paperSum}\) on the right exactly as printed.

Assuming 49: for every cutoff \(\rho \) there is \(\lambda _0(\rho ) {\gt} 0\) such that for all \(\lambda \in (0,\lambda _0)\) and every finite family of modes, the vectors \(\big(\widehat{\mathcal{H}_\varepsilon }(\alpha _j,\beta _j)\big)_j\) converge in distribution, as \(\varepsilon \to 0^+\), to the Gaussian limit law of 50.

For \(\tau \)-separated points \(x_1,\dots ,x_n \in \mathbb {T}^4\): \(\sum _{\pi \in S_n}\prod _{j=1}^{n-1} \lvert x_{\pi (j)} - x_{\pi (j+1)}\rvert ^{-2} \le C^n (n!)^{1/2}\tau ^{-2(n-1)}\), via the iterated local inequality (1.15).