4 The Syracuse random variable and its valuation
The law syracZ \(n\) on \(\mathbb {Z}/3^n\mathbb {Z}\) (paper (1.21)/(1.26), in the reversed variable order deliberately, per footnote 6): the pushforward of \(\mathrm{Geom}(2)^{\otimes n}\) under
where \(2^{-1}\) is the inverse of the unit \(2\) mod \(3^n\). With the projection compatibility (paper (1.22)): syracZ \(n\) pushes forward to syracZ \(k\) under \(\mathbb {Z}/3^n\mathbb {Z}\to \mathbb {Z}/3^k\mathbb {Z}\) for \(k\le n\); and the recursion Lemma 1.12 (Euler’s theorem plus a geometric-series normalization \((1-2^{-2\cdot 3^n})^{-1}\)).
Campaign estimate: 5–10 treadmill laps; risk low (85% confidence the node completes as stated).
Proposition 1.9. There are \(c_1,C{\gt}0\) such that for all \(n,n'\) and every law \(X\) supported on odd numbers that is \(\ll 2^{-n'}\)-close in total variation to uniform modulo \(2^{n'}\), provided \((2+c_0)n\le n'\),
I.e. the Syracuse valuation vector of an equidistributed-mod-\(2^{n'}\) input is exponentially close to \(n\) independent geometric variables. Includes the §4 tail bound Lemma 4.1 controlling \(\mathbb {P}(a_{[1,n]}\ge n')\). COMPLETE (judge pass 22, 2026-07-13). valuation_dist (Prop 1.9) and valuation_tail (Lemma 4.1) proved by an external Codex session and judge-verified: pinned statements character-untouched (constituent unifOddMod body unchanged; statements re-read vs Prop 1.9 p.7 / Lemma 4.1 p.22 — the \(\forall c_0,K\, \exists c_1,C\) quantifier structure matches the paper’s “constants may depend on \(c_0\)” exactly). The tail proof consumed the long-parked (1.10) hole PMF.abs_expect_indicator_sub_le_dTV (Prob/Basic), caught by the dated axiom run and discharged by the judge same pass. Dated runs 2026-07-13 on both headliners + valVec_pos, fnat_mod_two_of_pos, unifOddMod_map_valVec_apply, truncated_val_dTV_le, PMF.dTV_map_le — all exactly \([\texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}]\).
Route (paper §4, with one sound reordering): the event \(\vec a^{(n)}(N) = \vec a\) is classified as a single residue of \(N\) modulo \(2^{a_{[1,n]}+1}\) (via Lemma 2.1, node 3.2); pushing the equidistribution hypothesis through the truncation \(2^{n'} \to 2^{|a|+1}\) (data processing, PMF.dTV_map_le) matches the truncated valuation law with \(\mathrm{Geom}(2)^{\otimes n}\) exactly below level \(n'\); the overflow \(|a| \ge n'\) is controlled on the geometric side by the S2 tail engine. Lemma 4.1 is then derived from Prop 1.9 plus the geometric tail (reverse of the paper’s order — sound and non-circular, since \(\mathbb {P}_P(E) \le \mathbb {P}_Q(E) + d_{\mathrm{TV}}(P,Q)\) via the now-proved (1.10)).