5 First passage, stabilization, and the main theorem
5.1 The main theorem
Theorem 1.3 (the summit): for every \(f:\mathbb {N}\to \mathbb {R}\) with \(f(N)\to \infty \), \(\mathrm{Colmin}(N){\lt}f(N)\) for almost all \(N\) in logarithmic density. It follows from the intermediate Theorem 1.6 (almost all orbits attain almost bounded values) which in turn follows from the quantitative Theorem 3.1: there exist \(c,C{\gt}0\) so that for all \(N_0,x\ge 2\),
Thm 3.1 is obtained from the stabilization estimate Prop 1.11 (node 5.10) by iterating over dyadic scales (§3).
Campaign estimate: 0 treadmill laps; risk done (100% confidence the node completes as stated).
🏔️ THE SUMMIT (2026-07-15, 8ccd1a2/9f17733): both frozen Statement.lean stubs discharged by exact from the C6s spine — the only edit that file ever receives. Kernel-checked axiom-clean host-side, 114 declarations (blueprint_audit 2026-07-15, 0 drift, 0 false-green). Judge ratification reads still owed on the C6 pins (ratify-on-pin flags stand); flips under the trust-the-treadmill ruling.
Paper p.16, both displays of the one claim ("…or equivalently …"): \(\sum _{N\in 2\mathbb {N}+1\cap [1,x]:\ \mathrm{Syrmin}(N){\gt}N_0} 1/N \ll \log x/\log ^c N_0\), and \(\mathbb {P}(\mathrm{Syrmin}(\mathbf{Log}(2\mathbb {N}+1\cap [1,x]))\le N_0) \ge 1-O(\log ^{-c}N_0)\). Obtained from Prop 1.11 (node 5.10) by the dyadic-scale telescoping of §3 (pp.17–18).
Campaign estimate: 0 treadmill laps; risk done (100% confidence the node completes as stated).
Kernel-clean, BOTH forms (2c3e273+; blueprint_audit 2026-07-15 lists C6a on the MISSED-FLIP roll). Telescope \(\to \) covering \(\to \) sum/probability forms. Trust-the-treadmill flip (operator layer); judge flip-back allowed.
Paper p.4: for \(f\) with \(f(N)\to \infty \), almost all odd \(N\) (log density on the odd window) satisfy \(\mathrm{Syrmin}(N){\lt}f(N)\). From Thm 3.1 at \(N_0:=\tilde f(x)= \inf _{N\ge x}f(N)\) (p.18).
Campaign estimate: 0 treadmill laps; risk done (100% confidence the node completes as stated).
Kernel-clean (blueprint_audit 2026-07-15, MISSED-FLIP roll). Trust-the-treadmill flip (operator layer); judge flip-back allowed.
Worker-authored rendering of the one-paragraph reductions (p.5 and p.16 "in particular, by (1.2)"): quantitatively, \(\sum _{N\le x:\ \mathrm{oddPart}(N)\in A} 1/N \le 2\sum _{M\in A\cap (2\mathbb {N}+1)\cap [1,x]} 1/M\) (geometric series over \(\nu _2\)); qualitatively, an almost-all-odd property pulls back along \(\mathrm{oddPart}\) to almost-all on \(\mathbb {N}+1\). Rests on the proved \(\mathrm{Colmin}= \mathrm{Syrmin}\circ \mathrm{oddPart}\) (node 3.1). Trap: check15 (constant 2 exact and \({\gt}1.8\)-tight, so a constant-1 mis-rendering fails).
Campaign estimate: 0 treadmill laps; risk done (100% confidence the node completes as stated).
Kernel-clean, both forms (42fb97c half 1, 3de7831 half 2; blueprint_audit 2026-07-15). Trust-the-treadmill flip; judge flip-back allowed.
Statements byte-identical to the two frozen Statement.lean headlines; when these close, the frozen sorries discharge by exact (the only edit Statement.lean ever receives). Quantitative route: C6a(sum form) + C6c + harmonic-mass bounds on the full window. Headline route: C6b at \(\tilde f\) + C6c + \(\mathrm{oddPart}(N)\le N\).
Campaign estimate: 0 treadmill laps; risk done (100% confidence the node completes as stated).
Kernel-clean, both spines (8ccd1a2; blueprint_audit 2026-07-15). Statements byte-identical to the frozen headlines, so the stubs discharged by exact. Trust-the-treadmill flip; judge flip-back allowed.
Beyond the paper: Theorem 3.1 with BOTH slots closed — the explicit exponent \(c_{\mathrm{Tao}}\) and a closed (tower-valued, deliberately non-small) constant \(C_{\mathrm{assembled}} = \max (C_{\mathrm{spine}}(X_{\mathrm{spine}}), \log ^{c_{\mathrm{Tao}}}2)\), where \(X_{\mathrm{spine}}\) is the X-chase closure of the development’s cutoff tree (no existential exponent, constant, or cutoff on the proof path; explicitness contract per BIG_C_EXPLICIT_BOUND_PLAN.md, enforced by tools/ExplicitnessClosure.lean + big_c_cutoff_audit.py –complete).
Campaign estimate: 0 treadmill laps; risk low (100% confidence the node completes as stated).
Kernel-clean (axioms = the standard three, no sorryAx; host-verified 2026-07-17 — receipt in the source comment above this node). Delegation: tao_collatz_quantitative_spine_atCX at the closed cutoff, weakened to the exponent \(c_{\mathrm{Tao}}\) by monotonicity (_of_le); the \(N_0 = 2\) window is absorbed by the second max arm. BigCTower.lean then proves the readable ceiling \(C_{\mathrm{assembled}} \le 10\uparrow \uparrow 63\) (tenTower 62), rendered on the trusted surface as CTao + tao_collatz_quantitative_fully_explicit (Statement.lean).
5.2 First passage (§5)
The first-passage data: \(\mathrm{passes}(x,N)\) (\(=T_x(N){\lt}\infty \), the orbit reaches \(\le x\)), the passage time \(\mathrm{passTime}\), and the passage location \(\mathrm{Pass}_x = \mathrm{passLoc}\) (with the convention \(\mathrm{Syr}^\infty := 1\)); plus the log-uniform law \(\mathbf{N}_y \equiv \mathbf{Log}(2\mathbb {N}+1 \cap [y,y^\alpha ])\) (\(\mathrm{logWindow}\), \(\mathrm{logUnifOdd}\)) and the exponent \(\alpha = 1.001\) (paper (1.18)).
Campaign estimate: 0 treadmill laps; risk low (100% confidence the node completes as stated).
Paper (1.19): a log-uniformly chosen odd \(N_y\) in the window \([y,y^\alpha ]\) fails ever to descend to \(\le x\) only with small probability,
Tao’s route (§5 pp.20–21) runs entirely over proved machinery except for one new brick: the integral test \(d_{\mathrm{TV}}(\mathbf{N}_y \bmod 2^{n'}, \mathrm{Unif}) \ll 2^{-n'}\), which is exactly the hypothesis Proposition 1.9 (node C5) takes. Given it, Prop 1.9 supplies (5.4), Lemma 2.2 (node S3, two-sided) supplies the lower-tail bound (5.5) \(\mathbb {P}(|\vec a^{(n_0)}(\mathbf{N}_y)| \le 1.9 n_0) \ll x^{-c}\), and an explicit descent computation gives \(\mathrm{Syr}^{n_0}(\mathbf{N}_y) = O(x^{0.99}) \le x\) on the complement, with \(n_0 := \lfloor \log x / (10\log 2)\rfloor \) (5.1).
Campaign estimate: 10–18 treadmill laps; risk medium (75% confidence the node completes as stated).
Ratified and flipped at judge pass 30 (2026-07-14): the theorem is kernel-clean (\(\mathrm{propext}, \mathrm{Classical.choice}, \mathrm{Quot.sound}\)), clearing the pass-29 missed flip. The route closed as designed — the integral test discharges Proposition 1.9’s \(d_{\mathrm{TV}}\) hypothesis (5.4), the two-sided Lemma 2.2 tail gives (5.5), and an explicit descent yields \(\mathrm{Syr}^{n_0}(\mathbf N_y) = O(x^{0.99}) \le x\).
Proposition 5.2, the approximate formula (paper (5.8)) for the law of the first-passage location, built from the bookkeeping events \(\mathcal{A}^{(n')}\) (5.11), \(E'\) (5.10), and \(I_y\) (5.9), through the \(B_{n,y}\) equivalence chain relating the passage location to the affine images of the input window. This is where the Prop 1.9 geometric approximation is fed into the concrete window statistics.
Campaign estimate: 0 treadmill laps; risk done (100% confidence the node completes as stated).
🏆 COMPLETE (2026-07-15 overnight): the (5.16) window term closed via the integral test over C7’s classMass/windowMass machinery; the (5.17) stepback closed by the forward/reverse-leg split with the early-return event proved empty (0bea9d1). Kernel-checked axiom-clean by blueprint_audit 2026-07-15 (MISSED FLIP list, twice). Statement pre-ratified (pass 30), so this flip is the mechanical half — done by the operator layer per the DIRECTION.md operator note.
Proposition 1.11, the spine’s key input. With \(\alpha =1.001\) (paper (1.18)): there are \(c,C,x_0{\gt}0\) so that for \(x\ge x_0\), the first-passage location laws seen from two successive scales \(x^{\alpha }\) and \(x^{\alpha ^2}\) agree up to
together with the non-escape control on each window. Proved via Lemma 5.3 (\(c_n(X)\ll 1\)) and (5.18)–(5.21), applying the fine-scale mixing Prop 1.14 (node 6.1) at a base scale \(m_0\).
Campaign estimate: 0 treadmill laps; risk done (100% confidence the node completes as stated).
🏆 COMPLETE (2026-07-15, 9e5604b): assembly + every leaf closed; stabilization kernel-checked axiom-clean by blueprint_audit (MISSED FLIP list). Flipped under the trust-the-treadmill ruling (DIRECTION.md operator note); judge flip-back allowed.
\(|\mathrm{perNHarmonic}\, x\, E\, n - \mathrm{harmZfine}\, x\, E\, n| \le C(\log x)^{-c}\) on \(I_y\): the iid-geomHalf \(2^{-\mathrm{pre}\, \bar a}\) mass over good, affine-solvable tuples agrees with the exact \(\mathrm{Syrac}(\mathbb {Z}/3^{n-m_0}\mathbb {Z})\) mass. Both ribs (syracZ_sub_perNGoodMass_bound; the solvable_iff_fmapZ pointwise bridge) are proved; the assembly is L\(^1\times \)L\(^\infty \) Hölder against cn_bound. Does NOT consume C10.
Campaign estimate: 0 treadmill laps; risk done (100% confidence the node completes as stated).
Kernel-clean (44fcd94; blueprint_audit 2026-07-15). Trust-the-treadmill flip (operator layer); judge flip-back allowed.
\(|\mathrm{harmZfine}\, x\, E\, n - \mathrm{mainZ}\, x\, E| \le C(\log x)^{-c}\): L\(^1\times \)L\(^\infty \) Hölder, \(\sup _X c_n(X) \le C\log ^{0.7}x\) (cn_bound) against \(\mathrm{osc}\, m_0\, (n-m_0) \le C' m_0^{-A}\) via Prop 1.14 (node 6.1) at \(A {\gt} 0.7 + c\) – the SOLE consumption of C10 inside C9.
Campaign estimate: 0 treadmill laps; risk done (100% confidence the node completes as stated).
Kernel-clean (ece1f36; blueprint_audit 2026-07-15). Trust-the-treadmill flip (operator layer); judge flip-back allowed.
\(|\mathrm{perNTerm}\, x\, E\, y\, n - \mathrm{perNHarmonic}\, x\, E\, n/\mathrm{norm}| \le C(\log x)^{-c}/\mathrm{norm}\), \(\mathrm{norm} = \tfrac {\alpha -1}{2}\log y\): the affine mass collapses to the single point \(N^* = (M\, 2^{\mathrm{pre}\, \bar a} - \mathrm{fnat})/3^{n-m_0}\) (perNTerm_pointmass), which is odd (Nstar_odd, via fnat_odd) and lies on the window (Nstar_mem_logWindow, both PROVED this run), so \(\mathbb {P} = (N^*)^{-1}/D_y\); then \((N^*)^{-1} \approx 3^{n-m_0}/(M\, 2^{\mathrm{pre}})\) (relative \(O(x^{-c})\)) and \(1/D_y \approx 1/\mathrm{norm}\) (windowMass_estimate/windowMass_ge_clog), with relative errors made absolute by \(\mathrm{perNHarmonic} \le C\log ^{0.7}x\) (perNHarmonic_le, PROVED). Does NOT consume C10.
Campaign estimate: 0 treadmill laps; risk done (100% confidence the node completes as stated).
Kernel-clean (60bb490; blueprint_audit 2026-07-15). Trust-the-treadmill flip (operator layer); judge flip-back allowed.