6 Layer L3: deterministic parametrix
The deterministic content of the paper’s §3.1–§3.2 and all of §4: profile kernels, the renormalization induction, the constants \(\mathcal{C}_{2q}\), and the deterministic halves of Proposition 3.5.
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]\).
\(\mathcal{RI}\) at the deterministic level: repeatedly remove the smallest-leftmost fully paired subinterval, via \(J\) and \(\widetilde G\) ((3.3)–(3.5)).
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.
\(\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.
The explicit formula (3.12).
\(\lvert \mathcal{C}_{2q}\rvert \le \varepsilon ^{-2} \lvert \log \varepsilon \rvert ^{-1}(C\lambda )^{2q}\) for \(1 \le q \le A\).
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 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}\).
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).