- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
- Pale red background
- campaign risk: high (the node's PROOF is still open — the tint tracks remaining proof risk and drops only on completion; the border independently tracks statement status; label's second line = estimated treadmill laps)
- Pale amber background
- campaign risk: medium
- Pale green background
- campaign risk: low
- Tinted box, “support N–M” label
- a definition node whose bound defs compile and are ratified, but with N–M laps of support-lemma work still open in its files — it wears its campaign-risk tint (not status green) until that work is done, so a dark-green box always means no remaining work of any kind. Everything already consumed from such a node is #print-axioms-certified sorry-free, so descendants’ dark green stands.
The Collatz map \(\mathrm{col}(N)=3N+1\) if \(N\) is odd and \(N/2\) otherwise; its orbit minimum \(\mathrm{Colmin}(N)=\inf _k \mathrm{col}^{[k]}(N)\). The odd part \(\mathrm{oddPart}(N)=N/2^{v_2(N)}\), the Syracuse map \(\mathrm{syr}(N)=\mathrm{oddPart}(3N+1)\) (odd \(\to \) odd), and its orbit minimum \(\mathrm{Syrmin}\). The elementary reduction (paper (1.2)) that lets the entire problem be studied on the odd numbers:
Also the cheap odd-preservation and positivity facts (\(\mathrm{syr}\) maps odds to odds, etc.).
Campaign estimate: 3–6 treadmill laps; risk low (95% confidence the node completes as stated).
Proposition 1.14: the Syracuse law is asymptotically equidistributed at fine scales,
Deduced from the character-sum decay Prop 1.17 (node 7.11, the head of the §7 crux “X-chain”) by Plancherel on \(\mathbb {Z}/3^n\mathbb {Z}\). The §6 machinery around it: Lemma 6.2 (\(F_n\) injective), Cor 6.3 (\(3\)-adic separation of the offsets), the event \(E\) (6.2), the stopping time \(k\), and the Plancherel step.
Campaign estimate: 0 treadmill laps; risk done (100% confidence the node completes as stated).
The \(n\)-step valuation vector (paper (1.8)) \(\vec a^{(n)}(N)_i = v_2\bigl(3\, \mathrm{syr}^{[i]}(N)+1\bigr)\), the integerified offset (design D2) \(\texttt{fnat}\, n\, a = \sum _{m{\lt}n} 3^{\, n-1-m}\, 2^{\, a_{[1,m]}}\), and the load-bearing iteration identity, the paper’s (1.7) multiplied through by \(2^{|a|}\) so it holds in \(\mathbb {N}\): for odd \(N\), with \(a=\vec a^{(n)}(N)\),
(By induction on \(n\); the step is \(2^{a_{n+1}}\mathrm{syr}(\mathrm{syr}^{[n]}N) = 3\, \mathrm{syr}^{[n]}N + 1\).) Together with Lemma 2.1: the valuation vector is the unique tuple with all entries \(\ge 1\) making the affine quotient odd. COMPLETE (judge pass 21, 2026-07-13). valVec_unique (Lemma 2.1 as a hypothesis-guarded iff: divisibility \(\wedge \) odd quotient \(\leftrightarrow \) \(a = \texttt{valVec}\), for tuples with entries \(\ge 1\)) was proved by an external Codex session and judge-verified: statement RATIFIED vs Lemma 2.1 p.14 (RATIFY-2 resolved — the iff matches the paper’s uniqueness claim; the paper’s membership half, \(\vec a^{(n)} \in (\mathbb {N}+1)^n\) itself, is an unformalized one-line companion, consumer-safe since candidate tuples carry the hypothesis by construction); proof route is the paper’s own last-entry induction; dated judge runs 2026-07-13 on syr_iterate_key, valVec_unique, syr_iterate_odd all exactly \([\texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}]\).
The logarithmic-density apparatus: logSum, logProb, the sampling window Finset.Icc 1 x, the predicate HasLogDensity, and the “almost all” quantifiers AlmostAllPos and its odd-window form AlmostAllOdd (logarithmic density restricted to \(2\mathbb {N}+1\)). With the harmonic-sum integral tests (paper (5.25)(5.26)) and the elementary splitting reducing the even-index statement Thm 1.6 to the main theorem Thm 1.3 (node 5.1) by passing to odd parts.
Campaign estimate: 6–12 treadmill laps; risk low (85% confidence the node completes as stated).
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}]\).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
\(|\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).
\(|\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).
\(|\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).
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).
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).
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).
The character \(\chi \) (paper (7.1)) and the reduction of Prop 1.17 to a bound on \(\mathbb {E}\, \chi \) through the reversed form (1.26); the pairing \(b_j = a_{2j-1}+a_{2j}\sim \mathrm{Pascal}\) that groups the geometric valuations two at a time; and the conditional factorization (7.4)/(7.5) of the Fourier coefficient into a product of per-pair factors \(f\) (with the low-order piece \(g\) split off). Pinned + ratified 2026-07-12 (judge pass 10, lap 53, paper pp.33–35): cexpect_pairing is the (7.5) bound verbatim — LHS = the (7.2) reversed character sum over \(\mathrm{Geom}(2)^n\), RHS = the \(\mathrm{Pascal}^{\lfloor n/2\rfloor }\) expectation of \(\prod _j \| f(x_j,b_j)\| \), the \(|g|\le 1\) leftover drop built in, and no \(3\nmid \xi \) hypothesis needed (pure algebra, a harmless strengthening). fCond is (7.4) in concrete uniform-pair form (junk value \(0\) off Pascal’s support, documented); xArg carries the 0-based \(j\)-shift (RATIFY-4). Character algebra, (7.6), and Lemma 7.2’s exact value \(\| f(x,3)\| = |\cos \pi \theta |\) are proved; key_fourier_decay (Prop 7.1) moved drift-free from Holding.lean and is now a theorem from the pairing + damping + Prop 7.3, and charFn_decay (Prop 1.17) is derived across the (1.26) seam. COMPLETE (lap 53; judge pass 11, 2026-07-12): cexpect_pairing PROVED via the generalized pair-peel cexpect_pairing_gen (statement drift-free) and judge-verified \([\mathrm{propext}, \mathrm{Classical.choice}, \mathrm{Quot.sound}]\); Prop 1.17’s remaining trust runs only through the Prop 7.8 chain (white_cos_bound closed lap 54, judge pass 12).
Risk kernel 3b. Lemma 7.10 (paper (7.60)–(7.65)): after a lengthy crossing, large triangles are rarely encountered, by a separated-\(\Sigma \) counting argument over the triangle family (node 7.3) using the first-passage location law (node 7.6). This is the complementary tail to Case 2. Statement pinned + ratified 2026-07-12 (judge pass 8, paper pp.51–54): triangle_encounter_le states \(\mathbb {P}(E_{p,s'}) \le C A^2(1+p)/s' + C e^{-cA^2(1+p)}\) over the endpoint law \(\texttt{fpDistPlus}\; s\; p = \texttt{fpDist}\; s \star \texttt{iidSum hold}\; p\) — the D1 encoding of \(v_{[1,\mathbf{k}+p]}\); the strong-Markov identification is absorbed into the encoding, with the same trust status as fpDist itself. A-quantifier fix (lap 57, judge pass 18): the earlier \(\forall A{\gt}0\) pin was false — the (7.61) height display needs \(A^2\) to clear the per-step height mean \(16\) (hold_mean_snd); at fixed small \(A\) and \(p\to \infty \) the endpoint sits at height \(l_\Delta + \Theta (p)\) outside the \(A^2(1+p)\) window. The paper’s \(A\) is a standing large parameter. Old ratification REVOKED; the re-pin \(\exists A_0 \ge 1,\ \forall A \ge A_0\) (with \(C, c, A_0\) uniform in \(n,\xi ,F\)) is RATIFIED vs pp.51–52, consumer-safe (the p.54 union bound instantiates at one large \(A\); pass-15 read). The (7.61) tails are pinned separately and ratified as route pins anchored to the p.52 displays: fpDistPlus_height_tail (\(\le C e^{-cH}\) under margin \(50(1+p) {\gt} 16/\text{step}\) drift; the first \(10(1+p)\) pin was below the drift and self-caught same lap) and fpDistPlus_col_tail (Gaussian width \(\sqrt{1+s}\) + Chernoff under margin \(10(1+p) {\gt} 4/\text{step}\); the \(s^{0.6}\) arithmetic is the assembly site’s). The (7.65) apex-interval disjointness step (TriangleFamily.not_mem_two) is already proved from node 7.3’s separation — disjointness-based, so the pass-18 route escalation does not touch this node. Lap 58 (judge pass 19): both (7.61) tails are PROVED (judge-run clean), and the assembly is decomposed per pp.52–54: encounter_apex_proximity (X10a, the (7.63)\(\to \)(7.65) confinement — PROVED + ratified vs p.53, judge-run clean) + encounter_separated_sum (X10b, the p.54 \(\Sigma \)-band sum — pinned; the lap-59 regime hypothesis \((s')^2 \le 1+s\) is judge-pre-authorized as ratified-on-landing: without it the pin is false for \(s' \gg \sqrt{s}\), and the consumer’s standing \(s' \le m^{0.4}\), \(s {\gt} m/\log ^2 m\) supply it above an absolute threshold). Lap 59 (judge pass 20): COMPLETE. X10b’s regime fix landed character-exact to the pre-authorization (RATIFIED; discharge recorded in the pass-19 addendum) and was PROVED the same lap; the glue landed in lap 59’s final commit, relocating the pinned headline statement below its engines character-identically (judge-diffed across the move). Dated judge runs 2026-07-12 on all nine lap-59 declarations — X10b, both \(G\)-weight engines, the banded/qualifying steps, the three glue helpers, and the headline triangle_encounter_le itself — all exactly \([\texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}]\).
Judge pass 26 (2026-07-14): a deviation, caught and repaired — the *_rpow engine split. An unattended lap (61f8e80) rewrote the deep hypothesis of triangle_encounter_le (and X10a encounter_apex_proximity) from \(m/\log ^2 m {\lt} s\) to \(m^{0.8} {\lt} s\), to unblock the Case-3 consumer, whose triangle sits at row \(n/2-m-1\) (depth \(m+1\)) — and \(m/\log ^2 m {\lt} s \Rightarrow (m+1)/\log ^2(m+1) {\lt} s\) genuinely fails (\(x/\log ^2 x\) increasing; fractional-part counterexample). The route reasoning was right, but the edit was not a generalization: the two hypotheses are incomparable (\(m^{0.8} \le m/\log ^2 m\) only for \(m \gtrsim 10^{15.5}\); below that the new form covers fewer \(s\)), and Tao p.51 states Lemma 7.10 with \(s {\gt} m/\log ^2 m\) verbatim — so the node had stopped rendering the paper’s lemma while staying green and axiom-clean. Ratifications were REVOKED and the repair mandated: split, don’t revert. The four weaker-hypothesis lemmas are kept as *_rpow engines (which is what the Case-3 chain consumes), and the two pins were restored character-identically and re-proved as corollaries — \(m \ge 10^{27}\) via log_sq_le_rpow, \(m {\lt} 10^{27}\) trivially (a sub-probability \(\le 1\) against a bound a large \(C\) makes \(\ge 1\)), exactly the shallow branch this proof already uses. Discharged 4f51542: the judge’s character-differ reports 19/19 pinned statements byte-identical to the pre-deviation baseline, and dated runs 2026-07-14 on both restored pins and all four engines are exactly \([\texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}]\). Net: the campaign gained a strictly stronger engine and kept a faithful Lemma 7.10. Ratifications RESTORED.
Case 3 assembly (paper (7.48)/(7.49), (7.52)–(7.67)): the events \(E_*,F_*\), the choice \(R=\lfloor A^2/\varepsilon ^4\rfloor \), and the deterministic claim (7.67), combining Lemma 7.9 (node 7.9) and Lemma 7.10 (node 7.10). This closes Prop 7.8, hence Prop 7.3 (node 7.4) and Prop 7.1, hence the crux Proposition 1.17 (character-sum decay): for every \(A{\gt}0\) there is \(C{\gt}0\) with, for all \(n\ge 1\) and all \(\xi \) with \(3\nmid \xi \),
This is the single Fourier-analytic input the whole spine reduces to (feeds node 6.1). The Case-3 entry statement Q_black_edge_case3 ((7.53)–(7.67) interface, budget hypotheses matching (7.52) with the documented lattice slack) is judge-ratified 2026-07-12 vs pp.48–49 and consumed by the proved Q_black_edge split. Consumer checks pre-cleared (judge pass 15, pp.48–49 + 54–56 read): the (7.54) 0.9m split, the \(R := \lfloor A^2/\varepsilon ^4\rfloor \)-after-\(\varepsilon \) choice, the \(-O(A)\) Markov slack absorbing X9’s \(e^{2\varepsilon }\), the depth of every (7.67) encounter, and X10’s consumption at a single large \(A\) at the p.54 union bound (safe for the \(\exists A_0\) re-pin, judge pass 18). What remains at ratification time is pinning this node’s own statements (\(E_*, F_*\), (7.66)/(7.67), the assembly chain) when they land.
Campaign estimate: 10–20 treadmill laps; risk high — assembly volume; consumer geometry pre-cleared (75% (2026-07-12 judge pass 15) confidence the node completes as stated).
The phase \(\theta (j,l)\) (paper (7.7)/(7.8)), a signed fractional part of \(\xi \cdot 3^{2j-2}\cdot 2^{\, 1-l}/3^n\), and its two scaling identities (7.13)/(7.14): there are integers \(k\) with
The black/white dichotomy (7.9) with \(\varepsilon = 10^{-4}\): a point is black when \(|\theta (j,l)|\le \varepsilon \), white otherwise. Lemma 7.2 (white-point cancellation): at a white point the per-pair factor contracts, \(|f| \le |\cos (\pi \theta )| \le \exp (-\varepsilon ^3)\).
Risk kernel 2. With a triangle (paper (7.11)) the set \(\{ (j,l) : j_0\le j,\ l\le l_0,\ (j-j_0)\log 9 + (l_0-l)\log 2 \le s\} \), Lemma 7.4 asserts the black set inside the strip is a disjoint union of triangles that are (i) confined to the strip \(j+1\le \lfloor n/2\rfloor - \tfrac {1}{10}\log (1/\varepsilon )\), and (ii) pairwise Euclidean-separated by at least \(\tfrac {1}{10}\log (1/\varepsilon )\):
Proved through the phase identities (7.12)–(7.15), the weakly-black claims (i)–(iii), the \(l^*/j^*\) construction, and Claim (\(*\)) Cases 1–3.
The holding law \(\mathrm{Hold}\) on \(\mathbb {N}\times \mathbb {Z}\) (§7.3), whose first coordinate is always \(\ge 1\), governing how the renewal walk steps between pairs. Design decision D6 replaces the paper’s infinite renewal product (7.34) by the defined downward recursion \(Q:\mathbb {N}\times \mathbb {Z}\to \mathbb {R}\) (paper (7.35)),
well-founded on \(\lfloor n/2\rfloor - j\) (Hold’s first coordinate is \(\ge 1\)), with \(0\le Q\le 1\). The bridge (7.28)/(7.34)–(7.36) makes \(\mathbb {E}\, Q(\mathrm{Hold})\ll _A n^{-A}\) equivalent to Proposition 7.3 (the renewal white-encounter count, in the finite-vector form over \(\mathrm{Pascal}^{\otimes \lfloor n/2\rfloor }\)). This node exists to validate the D6 finitization.
Campaign estimate: 8–15 treadmill laps; risk medium (80% confidence the node completes as stated).
Lemma 7.6 (paper p.42): the explicit distribution of \(\mathrm{Hold}\), its exponential tail, aperiodicity, and mean vector \((4,16)\). These are the renewal-theory inputs (drift and spread) for the first-passage analysis of the walk. Clause map: exponential tail + the “in particular” Lemma 2.2 conclusion are the S3 engine (hold_tail_bound/hold_local_bound, proved directly by the paper’s own Chernoff route (7.29)–(7.30)); mean \((4,16)\) = hold_mean_fst/snd (direct sum over the explicit construction, \(\mathbb {E}\mathrm{Pascal}' = 13/3\) per (7.29)); aperiodicity = hold_aperiodic (support \(\subseteq x + H\) forces \(H = \top \), the paper’s own witnesses \((1,3)\), \((1,3)+(1,b)\)).
Lemma 7.7 (paper p.43): the first-passage endpoint mass satisfies \(\mathbb {P}(\mathbf{v}_{[1,\mathbf{k}]}=(j,l)) \ll e^{-c(l-s)}(1+s)^{-1/2} G_{1+s}(c(j-s/4))\). D6 form: fpDist (budget-recursive endpoint PMF, support facts proved) and fpDist_location_bound, judge-ratified vs the p.43 display 2026-07-10 (unconditional in \(l\) since the support fact kills \(l\le s\)). Uses the local 2-D bound (node 2.3) applied to the holding sums.
The truncated functional \(Q_m\) (paper (7.38)) and the skeleton of Proposition 7.8 (the quantitative white-encounter bound), together with Case 1 (paper (7.42)/(7.43)): when the walk starts at a white point, the \(e^{-\varepsilon ^3}\) contraction from Lemma 7.2 (node 7.2) already delivers the required decay. Judge-ratified 2026-07-10 vs pp.45–46: (7.38)\(\to \)Qm, (7.40)\(\to \)prop_7_8, (7.43)\(\to \)Q_white_case1 (verbatim incl. \(e^{-\varepsilon ^3/2}\)), (7.37)\(\to \)Q_polynomial_decay. Case 1 is proved; the skeleton delegates the black edge to Q_black_edge (nodes 7.8/7.10), whose Case-2/Case-3 split over the Lemma 7.4 triangle family is now itself PROVED (judge pass 6) — prop_7_8 is fully conditional on the two case statements alone.
Campaign estimate: 4–8 treadmill laps; risk low (85% confidence the node completes as stated).
Risk kernel 3a. Case 2 (paper (7.44)–(7.51), pp.46–48): the walk starts shallow inside a triangle (budget \(s\le m/\log ^2 m\)); the analysis produces the \(\gg 1\) white-exit bound (7.50)/(7.51) showing the walk leaves the triangle through a white in-strip point with absolute probability \(p_0{\gt}0\). Combines the triangle geometry (node 7.3), the first-passage location law (node 7.6), and the Case-1 contraction (node 7.7). Statements judge-ratified 2026-07-12 vs pp.46–48: the (7.46) endpoint step (subtraction-form damping, PROVED) and the (7.52) budget bound (PROVED, with documented lattice slack \(m+2\) for \(m\)); the two open kernels are the (7.48)/(7.49) weight degradation and the (7.50)/(7.51) white-exit mass — both consume node 7.6; the (7.47)-split assembly is mechanical bookkeeping once they land. The Lean white-exit form strengthens the paper’s “white” to “white and in-strip”, which the damping mechanism requires.
Campaign estimate: 8–16 treadmill laps; risk medium — risk kernel 3a, statements pinned (75% (2026-07-12 judge re-rate: endpoint step + budget PROVED axiom-clean; white-exit \(\approx 0.99\) Monte Carlo, \(\varepsilon \)-sites verified 2026-07-10) confidence the node completes as stated).
Re-pinned DEPTH-GATED + re-ratified (judge pass 14, 2026-07-12). The lap-55 truth challenge (judge-concurred: adversarial edge-strip families falsify the all-starts \(e^{2\varepsilon }\) — literature hole #6, sibling of #5; the paper’s own Lemma 7.9 inherits it through “(7.59) by repeating (7.51)”) is resolved by the box’s preferred fix: encStep gains a gate \(g\) (encounters count only at depth \(\ge g\) from the strip edge; \(g = 0\) recovers the prior encoding definitionally), and many_triangles_white binds \(g\) existentially. Consumer-safe: Case 3’s (7.54) surviving branch keeps every (7.67) encounter at depth \(\ge 0.1m \ge g\) once \(C_{A,\varepsilon } \ge 10g\) — judge-verified vs pp.48–49 + 54–56 (pass 15), along with the \(R := \lfloor A^2/\varepsilon ^4\rfloor \)-after-\(\varepsilon \) choice and the Markov \(-O(A)\) slack that absorbs the \(e^{2\varepsilon }\) constant. Remaining obligation: the proof’s \(\varepsilon _0\) must be \(\ge \) the dichotomy constant \(10^{-4}\) (the consumer instantiates there). Both deviations carry full docstrings with paper anchors. Lemma 7.9 (paper (7.57), pp.50–51): a walk crossing many triangles must encounter many white points — the banked white damping beats the \(\varepsilon \cdot \min (r,R)\) credit. Statement pinned + ratified 2026-07-12 (judge pass 8, lap 52; re-ratified pass 9 after the constant correction): the stopping-time data \((t_i, \Delta _i, r)\) is a left fold (EncState/encStep: position, clearing barrier, encounter count, running + banked white counts), and many_triangles_white states \(\texttt{encExpect} \le e^{2\varepsilon }\) for all horizons \(T\), all \(R \ge 1\), all \(\varepsilon \le \varepsilon _0\). Deviation from the paper (lap 52 route finding, judge-CONFIRMED pass 9): the paper’s p.51 conditional-expectation display banks white damping through the full first block (\(\sum _{p\le k_1}\)), but on stopped chains the true (7.57) sum ends at \(t_1 {\lt} k_1\) — and the discrepancy is typically the \(k_1\) exit-whiteness itself, the very term (7.59) cashes. The display under-states the true conditional expectation, so the derivation is unsound as written; the corrected pay-from-the-previous-block ledger has sharp toy value \(e^{\varepsilon }p_0/(1-(1-p_0)e^{\varepsilon }) \approx e^{\varepsilon /p_0} {\gt} e^{\varepsilon }\), hence the pin’s \(e^{2\varepsilon }\) (valid for \(p_0 \ge 1/2\); the p.55 consumer is Markov with \(R\) chosen after \(\varepsilon \), so absolute exponent constants wash out). Riders: (a) verify at node 7.11 that p.55 chooses \(R\) after \(\varepsilon \); (b) the \(2\varepsilon \) constant commits the proof to certifying \(p_0 {\gt} 1/2\) — now embodied in the pinned external input fpDist_white_exit_deep (judge pass 12, ratified vs the p.51 (7.59) reduction: identical to node 7.8’s Case-2 twin minus the budget hypothesis, which the paper’s “repeating the proof of (7.51)” at arbitrary triangle points licenses, with the (7.52) budget \(s = O(m)\) free from membership; the \(p_0 {\gt} 1/2\) mass demand is the corrected ledger’s documented deviation from the paper’s \(\gg 1\), Monte Carlo \(\approx 0.99\)). Other ratified deltas (pass 8): finite horizon \(\forall T\) (D6; T1 did NOT fire); \(\exists \varepsilon _0\)-family; index shift matching the Case-2 forms. Proved so far: geometric prerequisites, head-peel encExpect_succ, block bridge encExpect_block_le, coupling encExpect_anti (pass 9), and the corrected per-block ledger’s closed-form core (lap 54, pass 12): the chain value encChainX \(= p_0/(1-(1-p_0)e^{\varepsilon })\) with fixed-point identity, the cap \(X \le e^{\varepsilon }\) (whence \(e^{\varepsilon }X \le e^{2\varepsilon }\), the (7.57) constant), and the four-mass LP vertex analysis encounter_vertex_bound (maximum at \((0, 1-p_0)\) = the fixed point) — all axiom-checked. Lap 55 (judge pass 16): the \(Y/Z\) induction is CLOSED — many_triangles_white is proved with sorryAx trail exactly \(\{ \texttt{fpDist\_ white\_ exit\_ deep}\} \) (machine-checked); the kernel is the node’s sole remaining input. Mass numeral landed (lap 57, judge pass 17): the kernel is re-pinned at \(51/100 \le p_0\) (character-exact to the pass-16 pre-authorization), so \(\varepsilon _0 \ge 1/100 \ge 10^{-4}\) is provable by arithmetic — the consumer floor is discharged at the statement level. Kernel derived (lap 56): whiteness = in-strip \(\wedge \) outside-every-triangle, giving \(P \ge 1 - P(\text{out of strip}) - P(\text{in a family triangle})\); fpDist_col_le and fpDist_out_of_strip_le are PROVED (judge-run clean); the remaining tail is fpDist_any_triangle_le (family-triangle mass \(\le 1/8\)). ROUTE ESCALATION (lap 57, judge pass 18 CONCURRED): the formalized F.separated is vacuous at the frozen \(\varepsilon = 10^{-4}\): \((\tfrac {1}{10}\log 10^4)^2 \approx 0.848 {\lt} 1 \le \) any nonzero lattice distance\(^2\), and node 7.3 proves the clause by exactly that vacuity — while the paper’s (7.50) whiteness step consumes real separation \({\gt} O(1)\) (“at a distance \(O(1)\) from \(\Delta \), hence …white by Lemma 7.4”, constants independent of \(\varepsilon \)). Sound in the paper’s \(\varepsilon \)-sufficiently-small regime, unprovable at our D4 numeral — not a paper error. Consequences: the pass-17 route ratification of fpDist_any_triangle_le is WITHDRAWN (adversarial singleton-tiling families are interface-legal; no positive white-mass bound follows from the interface), and the fpDist_white_exit_deep statement ratification is SUSPENDED pending the altitude ruling: remedy (A) shrink \(\varepsilon \) + formalize the real Lemma-7.4 separation, or hybrid (B+A-small) — the vertical white gap white_gap_above_run_top (PROVED lap 57, judge-run clean: 13 white rows above any run top at the current \(\varepsilon \), exact-\(\mathbb {Q}\)) plus a smaller shrink for the horizontal residue. This node’s own statement (many_triangles_white) remains ratified; its proof is closed modulo the suspended kernel. Any D4 change fires the judge’s \(\varepsilon \)-sweep re-ratification tripwire (pass 18 list). ALTITUDE RULING (Trevor, 2026-07-12): Remedy A at \(\varepsilon = 10^{-90}\). The D4 numeral shrinks to \(10^{-90}\) — a rational power of ten (exact-\(\mathbb {Q}\) machinery preserved; never a transcendental like \(e^{-200}\)) giving separation \(\tfrac {1}{10}\log 10^{90} = 9\ln 10 \approx 20.7\), comfortably above any plausible p.48 \(O(1)\). The kernel route follows p.48 verbatim (paper-faithful ratification); the real Lemma-7.4 separation becomes content to formalize (node 7.3’s separation clause re-opens — sep_const_sq_le_one must die); the vertical gap lemma is kept (holds a fortiori, \(\approx 299\) rows at the new \(\varepsilon \)). Execution order: the ManyTriangles split lands first, then a dedicated D4-change lap (numeral + mechanical repairs only), then separation, then the kernel. Suspensions lift only via the post-sweep re-ratification. Pass 23 (2026-07-13): D4 change + real separation EXECUTED (external Codex session; split skipped — still queued): \(\varepsilon = 10^{-90}\) landed with all mechanical repairs, the full \(\varepsilon \)-sweep re-ratification ran (all seven armed items discharged; X2/X3/X10 re-verified clean at the new \(\varepsilon \)), and Lemma 7.4’s separation is now genuine content (node 7.3). ⚠️ SECOND ALTITUDE-CLASS ESCALATION (pass 23): quantifier order. The foreign-triangle tail fpDist_any_triangle_le was reduced (proved conditional: fpDist_any_triangle_le_of_localization_box) to the obligation \(\mathrm{sep} {\gt} \sqrt{X^2+Y^2}\) for an explicit X6-localization box — but the box proved via the \(16j - 5l\) negative-drift Chernoff has \(X \approx 2.6\cdot 10^6\), against \(\mathrm{sep} \approx 20.7\). ✅ Pass 24 (2026-07-13): escalation DOWNGRADED — not altitude-class. The p.48 re-read settles it. The paper’s (7.50) \(O(1)\) is a distance from \(\Delta \), not from the start point (the drift slope \(1/4\) is shallower than the edge slope \(\log 2/\log 9\), so the walk drifts along \(\Delta \)), and it is explicitly \(\varepsilon \)-free — and the committed geometry already renders exactly that (top-projection into \(\Delta \) via triangle_top_mem_add, then F.separated). The route is sound; the blocker is two throwaway constants. (i) fpDist_linear_tail bounds the \(16j-5l\) MGF with a quadratic penalty that near-cancels the \(-16\)/step drift, capping the tilt at \(1/20000\) (true ceiling \(0.213\)) and shipping \(B = 4\cdot 10^7\); the step law’s exact MGF (geomQuarter \(\times \) pascalNe3) gives \(B \approx 42\). (ii) fpDist_height_tail’s radius \(Y\) is existential (it sums X6’s envelope) — the real blocker — but is explicit via renewal-conv \(+\) strictly increasing heights (\(\Delta l \ge 3\), so each level is visited at most once: renewal mass \(\le 1\), no renewal theorem) \(+\) \(\Delta l\)’s exact MGF, giving \(Y = 139\). Box \(= \sqrt{47^2 + 139^2} \approx 147\) vs \(\mathrm{sep} \approx 20.7\): needs one cheap ruling, a numeral re-freeze \(10^{-90} \to 10^{-1000}\) (\(\mathrm{sep} \approx 230\)). D4-as-a-parameter is off the table; pass-23’s “\(10^7\)-digit numeral” was an artifact of the garbage \(B\). 🏆 COMPLETE (judge pass 25, 2026-07-13). The pass-24 diagnosis executed end to end in three treadmill laps. \(B\): \(4\cdot 10^7 \to 64\) via an exact Hold MGF closed form (tiltZ_hold_closed), freeing the Chernoff tilt from the quadratic box’s \(1/20000\) to \(1/16\) — and, as predicted, with no native_decide (the facts are real-analysis over \(\exp \)). \(Y\): existential \(\to \) 150, via fpDist_le_renewal_conv \(+\) strictly-increasing heights (renewal_level_le_one: each height level is visited at most once, so the renewal mass per level is \(\le 1\) — no renewal theorem, no local limit law) \(+\) \(\Delta l\)’s exact MGF; X6’s envelope constants were left existential, so the completed node was not re-opened. Box \(= \sqrt{51^2+150^2} \approx 158.4\) against \(\mathrm{sep} = 100\ln 10 \approx 230.26\) at the judge’s pre-authorized re-freeze \(\varepsilon = 10^{-1000}\) — it fits with \(\approx 45\% \) margin. fpDist_any_triangle_le is therefore a theorem, ManyTriangles.lean has zero sorries, and the pass-18/23 suspension on fpDist_white_exit_deep is lifted in the strongest way available: it is PROVED. Dated judge runs 2026-07-13 — fpDist_any_triangle_le, fpDist_white_exit_deep, many_triangles_white, fpDist_linear_tail_sharp, renewal_level_le_one — all exactly \([\texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}]\). The second of the two pinnacle kernels; both are now complete.