2 The support layer
Discrete-probability, generating-function, and Fourier scaffolding used everywhere below.
2.1 PMF calculus
Total variation distance \(d_{\mathrm{TV}}(p,q) := \sum _a' |(p\, a).\mathrm{toReal} - (q\, a).\mathrm{toReal}|\), real and complex expectations \(\mathbb {E}_p[f] := \sum _a' (p\, a).\mathrm{toReal}\cdot f(a)\), and the \(n\)-fold i.i.d. product \(p^{\otimes n}\) on \(\mathrm{Fin}\, n\to \alpha \) (node D1). Together with the coupling inequality (paper (1.10)), stated in indicator-expectation form to avoid OuterMeasure friction: for any event \(E\subseteq \alpha \),
Basic algebra of \(d_{\mathrm{TV}}\) (symmetry, non-negativity) and the support/apply lemmas of the i.i.d. product are part of this node.
Campaign estimate: 8–15 treadmill laps; risk low (90% confidence the node completes as stated).
2.2 The geometric family and local bounds
The lattice laws driving the Syracuse valuation: \(\mathrm{Geom}(2)\) with \(\mathbb {P}(a)=2^{-a}\) for \(a\ge 1\) (geomHalf); \(\mathrm{Geom}(4)\) (geomQuarter); \(\mathrm{Pascal}\), the law of \(a_1+a_2\) with \(a_i\sim \mathrm{Geom}(2)\), i.e. \(\mathbb {P}(b)=(b-1)2^{-b}\) for \(b\ge 2\) (pascal); and its conditioning off \(b=3\) (pascalNe3). The load-bearing computation is the exact negative-binomial point mass for the sum of \(n\) i.i.d. \(\mathrm{Geom}(2)\) variables,
(compositions of \(L\) into \(n\) positive parts), together with the moment generating functions and the one-dimensional Chernoff upper-tail bounds derived from them.
Campaign estimate: 6–12 treadmill laps; risk low (90% confidence the node completes as stated).
Risk kernel 1. Lemma 2.2(i)(ii): local-limit / Gaussian-type upper bounds on the point masses of sums of \(k\) i.i.d. copies of the relevant lattice distributions (\(\mathrm{Geom}(2)\), \(\mathrm{Geom}(4)\), \(\mathrm{Pascal}\), and the holding law \(\mathrm{Hold}\) of §7), uniform in the shift, of the shape \(\mathbb {P}(S_k = v)\ll k^{-d/2}\) with \(d\) the lattice dimension; together with the weight function \(G_n\) (paper (2.2)). Proved not by the paper’s contour/Morera route but by explicit generating functions plus real-variable exponential tilting (design decision D5): for the \(d=2\) holding sums this is the circle-method form \(\mathbb {P}(S_k=v)=(2\pi )^{-2}M(\lambda )^k e^{-\lambda \cdot v}\int _{[-\pi ,\pi ]^2} |\varphi _\lambda (t)|^k\, dt\) with \(\varphi _\lambda ,M\) explicit rational functions. Statements judge-ratified 2026-07-12 vs pp.14–15: per-instance forms in Prob/LocalInstances.lean (scalar) and Sec7/HoldLocal.lean (\(d=2\) Hold, with the correct \((n+1)^{-1}\) prefactor and product norm fed to the scalar \(G\)); the \(G_{1+n}\)-for-\(G_n\) index is constants-equivalent (in-paper precedent: Lemma 7.7).
Risk kernel 1 CLOSED (campaign laps 22–45; judge pass 5, 2026-07-12). All eight obligations — (i) and (ii) for \(\mathrm{Geom}(2)\), \(\mathrm{Geom}(4)\), \(\mathrm{Pascal}\), \(\mathrm{Hold}\) — machine-checked via the D5 route (circle-method inversion, character decay, exponential tilting, second-order MGF bounds with exact means, \(\lambda \)-clip Chernoff assembly), plus the generic engines iidSum_nat_local_of_quad / iidSum_nat_tail_of_quad. Judge-run #print axioms on all ten declarations (2026-07-12): [propext, Classical.choice, Quot.sound] — nothing extra.
2.3 Fourier analysis on \(\mathbb {Z}/3^n\mathbb {Z}\)
The additive character \(e(\theta ):=\exp (2\pi i\theta )\) on \(\mathbb {Q}\), the discrete Fourier transform and Parseval identity on \(\mathbb {Z}/3^n\mathbb {Z}\), and the oscillation functional \(\mathrm{Osc}_{m,n}\) (paper (1.24)) measuring how far a weight \(c:\mathbb {Z}/3^n\mathbb {Z}\to \mathbb {R}\) is from being constant on the fibres of the projection to \(\mathbb {Z}/3^m\mathbb {Z}\):
Includes the Remark 1.18 triangle inequality that lets \(\mathrm{Osc}\) be controlled scale by scale.
Campaign estimate: 4–8 treadmill laps; risk low (85% confidence the node completes as stated).