9 Layer L6: assembly
The external input, the limit law, the finite-mode reduction, and the conditional main theorem (paper §3.4 Steps 2–3 and Theorem 1.1).
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 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.
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.
Characteristic functions of the full resolvent modes converge once the second-moment input and the measurable good-event data are supplied; the good-event data are constructed from the deterministic bounds.
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)).
Fixed-truncation joint moments converge to Gaussian moments by Proposition 3.6; characteristic functions follow by the moment method; the truncation is removed by the geometric second-moment bound and the \(B \to \infty \) tail, with the even-term series summed to the limit prefactor.
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.