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.

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.

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.

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.