/machines/1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF/notes.md · raw

1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF

Status: KILLED_NONHALT (2026-10-10; see ## Kill at the bottom) Class guess (agent / Dennis): Counter Class 4: a recursive run-length counter whose epochs double in time / (pending) Spreadsheet notes / Discord thread: - Results tab row 832: status blank, class Counter Class 4, no notes, no links. - Level 0: note "-". Direct Simulation: in Group 25, not simulated to 1e14 (not struck through). - Not in either local Discord list (dyuan01 longitudinal 24, mxdys UBRRBA 86). - Twin 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB (Results row 833) is only tm' in Eqv.v TM113 and is unsolved. - Discord code A (#bb6 search) can't be checked locally. A ready-to-paste question is in observe.json discord_check. Viewer: https://bbchallenge.org/1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF

Observation

Diagrams are in img/: blaze_1e7, blaze_long_epoch_k8, records_1e9, default_site, plus viewer.html. Exact start/rows/window/colours are in observe.json diagrams. - blaze_long_epoch_k8.png (made by scripts/diagram_long_epoch.py) is the real run's k=8 long epoch, from Fl(8,10) at step 320,794 to Fs(9,4) at step 642,526. r1 loses its cells (17 → 1) at 421, 640, 1171, 2182, 2581, 4640, 5071, 9586, 10049, 19596, 20103, 39926, 79697, 80244, 160151, 160766 and 321721 steps into the epoch, so the waits double. - It replaces countdown_k8.png, which started from a constructed Fl(8,4) and kept only the A-entries where a heuristic said A was on run 1 or 2 (60 of 16,111 rows, unevenly spaced in time). - records_1e9.png mixes two kinds of row. Left-record rows show the compact epoch form, with two lone marker 1s on the right. Right-record rows catch the tape mid-epoch and show as long white bars. Its last new cell is at step 660,597,554. Rows are records, not time, so the picture cannot show the log growth.

Run-level model. The tape is runs of 1s. A reads the last cell of run r_p. Gaps left of it are single 0s, and there is a 00 gap after r_{p+1}. Four rules (below) reproduce the TM exactly at every A-entry. Checked against the TM at 1e4, 1e5, 1e6, 1e7, 5e7 and 2e8 steps (6/6 identical; 10M macro steps with no unhandled case).

Epochs (A at the left edge after R2e): - Fs(k,P) = 0^inf <A 0 1^3 0^2 1^2 0^2 1^(2k) 0^2 1^(2k+1) 0^P 1 0^Q 1 0^inf, with P+Q=2k and P, Q even. - The short epoch goes to Fl(k,P) = ... 1^3 0^2 1^(2k+1) 0^2 1^(2k+3) 0^2 1 0^P 1 0^Q 1 ... (P unchanged). - The long epoch (~1260·2^k steps) goes to Fs(k+1,P') or to the degenerate D(k+1). - Inside the long epoch, r1 counts down 2k+1 → 1. Each odd value costs one mini-epoch on the right side, and the mini-epochs double in length. This is the self-similar part.

History (k, P, Q) at Fs, from step 18826: (4,2,6) (5,6,4) (6,4,8) (7,4,10) (8,10,6) (9,4,14) (10,8,12) (11,12,10) (12,4,20) (13,12,14) (14,20,8) (15,24,6) (16,18,14) (17,30,4) (18,16,20) (19,14,24) (20,26,14) (21,10,32) (22,28,16) (23,38,8) (24,24,24), then D(25) at step 4.2e10, then Fs(26,2,50) at 8.5e10. The real orbit takes the D branch, just as the rules predict.

P looks irregular, but halting does not depend on it: - Every even P for k = 3..13 closes the long epoch with no halt (macro model). - Odd P (never reached) sometimes halts. - Random off-family tapes halt in 84–90% of 600 tries, so the invariant has to be specific to this family.

Candidate rules

All were tested by direct simulation from concrete configurations at random small, mid and large parameters.

R1   1^(n+2) <A 0 1^(m+1) 0^2 1^x 0  -->  1^(n+1) 0 1^(m+1) <A 0 1^(x+1) 0^2   3m+2x+15 steps  [60/60]
R2   1^(j+1) 0 1^(k+1) 0 1 <A 0      -->  1^(j+1) <A 0 1^(k+2) 0^2           k+10 steps      [60/60]
R2e  0^inf 1^(k+1) 0 1 <A 0          -->  0^inf <A 0 1^(k+2) 0^2             k+10 steps      [60/60]
R3   0^inf <A 0 1^(k+1) 0^2 1^m 0    -->  0^inf 1^(k+2) <A 0 1^(m+1) 0^2     3k+2m+11 steps  [60/60]
HALT 0^3 1 <A 0                      -->  halt (4 steps)                                    [40/40]
Fs(k,P) --> Fl(k,P)                                    40k+288 steps                      [24/24, k<=200]
Fl(k,P) --> Fs(k+1,P') (P' even) | D(k+1)              ~1260*2^k steps                    [22/22 TM; all even P k<=13 macro]
D(k)    --> E(k) = <A 0 1^3 0^2 1^(2k+3) 0^2 1^(2k+3) 0^2 1   40k+312 steps                [8/8]
E(k)    --> Fs(k+1,2)                                                                     [8/8]

Template check: no. CounterClass2v1 differs in 10 of 12 transitions, CounterClass3v2 and the closest CounterClass1 machine in 8. Starting from CC2v1's SkelE/Be shapes, this machine halts in 7 of 16 tries. Only CC2v1's proof skeleton (Inductive Side, Good invariant, progress_nonhalt_cond) is reusable.

Open: a P-independent invariant for the right side during the long epoch's countdown.

Checkpoint A (Dennis)

(pending)

Informal proof

Not started (waiting on Checkpoint A).

Formalization log

Not started.

Outcome

Open.

Card data pass (2026-10-10)

The card now shows at most 3 short mechanism bullets and yes/no questions that point at figures by number (primary figures first). The text they replaced is kept here. - Figure order on the card: Fig 1 = img/blaze_1e7.png, Fig 2 = img/blaze_long_epoch_k8.png, Fig 3 = img/records_1e9.png, Fig 4 = img/default_site.png (Figs 1-3 primary). - Mechanism, full observer version: - Tape = runs of 1s. Gaps left of the pointer (A) are single 0s, and a 00 gap sits just right of it. - R1: A moves one run right. Its old run loses a 1, the run past the 00 gains one, and the 00 moves right. - R2: when A sits on a lone 1, it merges into the run on its left and A jumps two runs back. R3: at the left edge the tape grows by one cell. - Halting needs A on a lone 1 at the far left (0^inf 1 1, and its losses come at times that double (~5k, 10k, 20k, 40k, 80k, 160k, 320k steps in). Read as one outer decrement per doubling inner mini-epoch? - blaze_1e7.png: given a likely ~100 KB proof, should this machine continue to the informal proof now?

Deepen pass (overnight 2026-10-10)

Result: confidence stays med. Most of the mechanism is now an exact recursion with validated rules. Non-halting still needs one counting invariant (the cost accounting below), which is not proven. Not a cryptid on current evidence. New scripts are in scripts/: runmodel.py, check_runmodel.py, model_history.py, short_epoch.py, tm_check_short.py, baselemma.py, baselemma2.py, tm_check_base.py, recursion_check.py, frame2_seq.py, longmap.py, allP.py, family_robust.py, de_check.py, and base_events.py (exploratory).

Notation. The run model keeps two lists. - Stack L: the runs left of A, separated by single 0s. A sits on the last 1 of the top run; frame p = len L. - Word R = [c1, g1, c2, g2, ...]: the runs and gaps right of A. - Edge word W: 0^inf <A 0 1^3 0^2 W, i.e. L = [], R = [3,2]+W. - S-word = [2,2,a,2,b]+M. T-word = [a,2,b]+M. M is a marker word (lone 1s and gaps). - In this notation: Fs(k,P,Q) = S(2k,2k+1)+[P,1,Q,1], Fl = T(2k+1,2k+3)+[2,1,P,1,Q,1], D(k) = S(2k+2,2k+1), E(k) = T(2k+3,2k+3)+[2,1]. - Ep(W) is one edge epoch: run from L=[], R=[3,2]+W until L=[] again, ending at R=[r,2]+W'. - r=3: frame 1 used 2 decrements ("cost 2"). r=2: it used 3 ("cost 3"). - A further return to frame 1 is the HALT (0^inf 1 <A).

Closed this pass (validated): 1. Run model = TM. It matches the TM at every macro step for 3,000 steps from step 18,826. Its summed step counts reproduce the TM history exactly (steps, P and Q) for Fs(5)..Fs(21), up to step 2,642,404,258. 2. Short epoch, general form. Ep([2,2,a,2,b]+M) = (3, [a+1,2,b+2,2,1]+M), in 18 macro steps and 12a+8b+280 TM steps. - Holds for all a,b >= 1, with M empty or its first gap >= 2. - Checks: 2,800/2,800 in the model; 60/60 on the TM directly (a,b up to 400; tm_check_short.py). - Covers Fs->Fl (40k+288) and D->E (40k+312). It fails only when M's first gap is 1, which the family never has. 3. Translation (base) lemma. Take any word W with Ep(W) = (r, W') and c = 5-r, any stack context L0, any y >= 2 and any z >= c+1. Then L0+[y] | [z,2]+W reaches L0+[y-1] | [z-c+1,2]+W' in the same number of macro steps, and frames below are untouched. - Why: R1 and R3 act the same way on R[1:]. Lower frames are read only when the pointer drops to them. Frame f+1's value matters only if it reaches 1. - Checks: 3,000 random words in the model (baselemma2.py, costs 2 and 3 both seen); 24 inner-context instances on the TM (tm_check_base.py). 4. Long epoch = replay. Take a T-word W=[a,2,b]+M with a >= 2 and M empty or its first gap >= 2. - A 7-macro-step transient leaves frame 2 = a, z = b+2 and inner word W_1 = [1]+M. - Then (r_i, W_{i+1}) = Ep(W_i) at base frame 2, with c_i = 5-r_i and z_{i+1} = z_i-c_i+1, for i = 1..a-1. - If z_i >= c_i+1 throughout, then Ep(W) = (3, [z_a,2]+W_a). - Checks: 405/405 random T-words where the hypothesis holds, 0 disagreements (recursion_check.py, seeds 0 and 1). - Meaning: the long epoch from Fl(k) runs the machine's own history again, starting from [1,P,1,Q,1] at frame 2, for 2k inner epochs. The inner level j climbs from 1 to about k, and the old markers ride along as the tail of the word. This is the self-similarity in Fig 2. - Example: the frame-2 sequence of the k=8, P=10 epoch is T(1,1), T(3,1), T(4,3), S(3,3), T(4,5), S(5,5), T(6,7), S(7,7), T(8,9), D(4), E(4), E(5), Fs(6), Fl(6), S(17,15), T(18,17) (frame2_seq.py 8 10). 5. Cost accounting. For Fl(k), z_a = 5 - (number of cost-3 inner epochs). - The result has head 3,2,2,2 (Fs(k+1) or D(k+1)) exactly when that number is 3. - If it is 2, the result is a different T-word. If it is 4 or more, frame 2 runs out early and the edge epoch costs 3 or halts. - Observed: every even P, k = 3..17 (135 cases), has exactly three cost-3 inner epochs, and every case ends in Fs or D with no halt (allP.py; table in scripts/allP_k3-17.txt). The k=18 row was still running when this was written. - The three are: T(3,1) next to the transient, one E-type T(a,a) epoch in the middle (its place depends on P), and the last inner epoch (x=2). 6. D->E->Fs(k+1,2,2k) holds for every k = 1..16 (de_check.py; the observer had 8/8). 7. Cost of E(j)+[g,1] (one extra marker after E's lone 1). The cost is 3 exactly when g <= 2j, and 2 when g >= 2j+2. Checked for j = 1..8, g = 2..20. - This is a clean "absorb the marker if it is within reach" threshold. - It suggests that cost-3 events are marker absorptions. Fl(k,P,Q) always has its markers inside reach (P+Q = 2k), so the count of 3 would not depend on P. 8. P->P' map. Tabulated for all even P, k <= 17. It is irregular but injective (the dynamics is injective). Halting does not depend on it at the outer level.

Still open (why not high): - A proof that the replay at every depth has the right number of cost-3 inner epochs. Formally: z_i >= c_i+1 throughout, and z_a = 2 for Fl/E-type words. - Cost 3 at one level means z runs out at the next level down, so this is a nested counting statement over marker words. - Candidate invariant: "an inner replay at level j absorbs exactly the markers within reach about 2j, at one cost unit each, and creates its new markers inside the next window". Item 7 is the first evidence for it. It is not yet stated in general or checked. - The invariant has to be specific to the reachable marker words. In family_robust.py, Fs(k,P,Q) plus a random tail of extra even-gap lone 1s halts in 10/300 trials, all with the tail starting [2,1,2,1]. "Any even-gap marker word" is therefore false. - Cryptid check: halting avoidance is exact (always exactly 3, never 2 or 4, for all 135 (k,P)). The irregular P' only feeds the next epoch. This looks structural, not pseudo-random. It would turn cryptid-like only if the invariant had to track P' itself.

Next step suggested: state and test the absorption-count invariant. For each S/T head type, find the cost as a function of the first marker's gap relative to reach, as item 7 did for E. Then check that the replay of [1]+M keeps every marker word inside that table. If it closes, proof.md can be written as an induction on k using lemmas 2-4.

Deepen pass 2 (overnight 2026-10-10)

Result: confidence high, recommend proof. Round 1's open counting invariant is now one clean law, the absorption law. It held on ~28k random marker words with 0 failures. With it, non-halting comes down to one fact: the top-level edge words are the marker-free orbit, and that orbit never pays cost 3. Not a cryptid: the irregular P' never enters the argument.

New in scripts/: - epc.c: the run model in C, with ep / orbit / c3 / abs / allP modes. It matches runmodel.py on allP k=3..12 and on orbits. - exhaust_check.py, exhaust_kinds.py, position_check.py (output in position_check_out.txt), u_rule_check.py. - absorption_out.txt, allP_k18-25.txt. - census.py: exploratory census of every push at every depth. Superseded by the orbit view.

Orbits. Take a marker word M: lone 1s with gaps g_1..g_m >= 2. - O_n(M) = Ep^n([1]+M). The cost of step n is the cost of Ep(O_n), which is 2 or 3. - The frame-2 replay inside a T-epoch is exactly O(M) (round-1 item 4). - The top level is O(∅). At TM step 50 the tape is L=[], R=[3,2,1], so the edge word is [1]. - Ep^n([1]) = [2,2,1], D(0), E(0), D(1), E(1), Fs(2,2,2), Fl(2), D(3), E(3), Fs(4,2,6), Fl(4), Fs(5,6,4), ... (checked to n=39; it is the observe history). - Absorption indices: I_j(M) = sum_{i<=j} (g_i - 1). Example: [2,1,P,1,Q,1] has I = 1, P, P+Q-1.

Closed this pass (validated): 1. Absorption law (AL). Ep(O_n(M)) never halts. It costs 3 exactly when n is in {I_1..I_m}, and 2 otherwise. - Checks: epc abs ran 27,908 random orbits (m=1..6, each to I_m+4..8 epochs), 0 failures. That is 15,655 orbits with even gaps, plus 12,253 that also allow odd gaps 2..13: AL holds there too, though the word shapes do not. - For Fl(k,P,Q) it predicts cost-3 replays at 2, P+1 and 2k. These are round 1's "exactly three" (T(3,1), the E-type one in the middle, the last one), now with their positions explained. - Clean small cases: [g,1] gives cost 3 at n=g-1 (g=2..23). [g1,1,g2,1] gives n = g1-1 and g1+g2-2 (63 pairs). Three markers: 120 triples, all as predicted. 2. Shape and e-law (even gaps). Every O_n is one of three word types, with lone markers and gaps >= 2: - a U-word ([1]+M, only at n=0), an S-word or a T-word. - S-words need a >= 2, so [2,2,1,2,..] reads as T(2,1). - At S/T words, e = #markers - (b-a+1) [S] or #markers - (b+1-a) [T]. - e always equals #{j : I_j >= n}, the number of original markers not yet absorbed. - 307,830 orbit words, 0 failures. It fails with odd gaps, which never occur on this machine. 3. Positional invariants at T-words O_n = [a,2,b]+M_n, where aff = b+1-a is the number of markers the replay can absorb and still end at z=2 (position_check.py, 2,400 orbits). - INT: the first aff markers of M_n are within reach, I_aff(M_n) <= a-2 (21,034/21,034). - EXT: let j be the first unabsorbed original marker. For n < I_j, the next marker sits at I_{aff+1}(M_n) = (a-2) + (I_j - n - 1). Its slack drops by exactly 1 per epoch (14,039/14,039). - TAIL: the later original markers keep their gaps g_{j+1}, ... (14,039/14,039). - ABS-STEP: at n = I_j, that marker is within reach, or it has merged into the head (aff = -1) (6,215/6,215). - The cost law also held at all 46,069 epochs. 4. z-accounting (pure arithmetic from round-1 item 4). - If the replay of T(a,b)+M absorbs exactly aff markers within replays 1..a-1, then z_i >= c_i+1 throughout and z_a = 2. The epoch costs 2 and the result [2,2]+W_a is an S-word. - If it absorbs aff+1, z first fails at the last replay, with z=2. 5. Exhaustion rule X (closes round 1's missing regime). Suppose the last replay child is pushed with z=2. Its cost would be 2 (ALPHA) or 3 (GAMMA). Then: - Ep([a,2,b]+M) = (2, [a''+2, 2, b''+2, g''+2] + rest), where W_{a-1} = [a'',2,b'',g'']+rest. - Derivation: the z=2 child kills its own C1, then suicides. That kills C2, so F pushes C3 = 2. C3's only child is killed at once, so C3 suicides, and F dies at value 1. Cost 3. - Checks: random T-words, 88/88 (exhaust_check.py; the round-1 no-exhaustion rule also held 979/979). Every absorption step in orbits, 1,345/1,345 (ALPHA 1,162, GAMMA 183; exhaust_kinds.py). - The other exhaustion kind (BETA: z=3 at the last replay; cost 3, and the result has a gap of 3) was seen only on random off-family words, never in an orbit. 6. U rule and the a=1 T rule (u_rule_check.py). - U rule: Ep([1]) = (3,[2,2,1]), and Ep([1,g]+rest) = (3,[2,2,1,g-2]+rest) for g >= 4 (600/600). - T rule at a=1: Ep([1,2,b]+M) = (3,[b+2,2,1]+M) (600/600). With the S rule (= T rule at a=2), every edge-word type is covered. 7. allP extended (C model) to k=18..25 for every even P: 164 more cases. - Every case has exactly 3 cost-3 frame-2 epochs and closes to Fs(k+1) or D(k+1). - In total: 299 (k,P) cases for k=3..25.

Non-halting argument. - Halting means the edge frame (value 4) gets three children killed, i.e. a top-level epoch of cost 4. - The top-level edge words are O_n(∅). AL with m=0 says every top-level epoch costs 2. So the TM never halts. - AL itself is proved by strong induction on n, simultaneously for all M: - U and S words cost 2 by closed rules. By items 2-3, n is never in I(M) at those words. - At a T-word, the replay is O(M_n) run for a-1 < n epochs. So the induction hypothesis gives the replay's cost-3 positions, I(M_n). - INT and EXT with slack >= 0 mean exactly aff markers are absorbed. By item 4, the cost is 2 and the result is an S-word. - At n = I_j, ABS-STEP adds exactly one absorption. By item 5, the cost is exactly 3. - How the invariants propagate: - S -> T: every I shifts by one and [2,1] (I=1) is prepended. - T -> S: the result's markers are those of the inner orbit word W_{a-1}. INT/EXT/TAIL hold for that inner orbit at step a-1 (induction hypothesis), so the internal markers stay within reach and the outer external slack drops by 2 over the two epochs. - T -> T at cost 3: rule X. - The irregular P -> P' map only ever appears inside the INT inequality, never as an exact value.

Still open (for proof.md, not observation): - Write the induction above in full. In particular, prove that INT/EXT/TAIL survive rule X and that W_{a-1} has T-parity. Both are validated here, not proven. - The formal proof will be large: a nested induction over marker words. It needs the TM-level lemmas R1/R2/R3, the translation lemma, the T/S/U/X epoch rules, and AL.

Informal proof (overnight 2026-10-10)

proof.md is written, and check_proof.py checks every claim in it (sections A–G). status.json is now stage informal_proof, status OPEN. Checkpoint B (Dennis, non-blocking) is pending.

What changed relative to deepen 2. The deepen-2 sketch had gaps; they are now closed: - Rule X is derived, not just validated. The exhaustion run from conf([2,2], [2,2]+T(a'',b'')+rest) is 10 explicit macro steps. It does not depend on whether the would-be inner cost is 2 or 3 (ALPHA/GAMMA). - BETA cannot happen. At an absorption step the absorbed marker sits at <= a-3, so ζ = 2 exactly at the last replay. - The invariant now covers the merged case. Deepen 2's EXT ("next marker at (a-2)+(I_j-n-1)") fails in two places: - at an absorption step: the marker is only within reach, or merged into the head; - at the S-word just before an absorption step, where aff = -1 also occurs (e.g. M=[10,1], n=8: S(9,7)). - The refined Inv(M,n) (proof.md §3) is: exact positions for every unabsorbed marker except the one being absorbed, which only has to be within reach (<= a-3); aff = -1 is allowed only at the absorption step (T) or one step before it (S). This version closes under all four transitions (U, S, T not at an absorption step, X). - b-law: b = n + α at T-words (n-1+α at S-words), with α = the number of absorbed markers. It gives the induction measure: - an inner replay at (N, a-1) has (a-1) + #N = n + m; - so strong induction on n + #markers is well-founded; - plain induction on n is not, because a-1 > n can happen (e.g. O_1([2,1,4,1]) = T(3,1)+[4,1]). - Parity: b is odd at every orbit word, and I_i ≡ i (mod 2) for even gaps. Together these show that the replay's final inner word is a T-word, which was the "T-parity" gap in deepen 2. - TL (translation) has a written proof: a step-by-step simulation relation with stacks [4-i]+S and L0+[y-1, z-i]+S.

Formalization plan (proof.md §7): - TM layer: shift rules CW, DW, FW, then R1, R3, R2, R2e over arbitrary sides. - lside/rside Fixpoints, with an RM_sound bridge. - A pure list nat model layer: mstep, Ep, U/TR/TL/TF/X, then Inv/AL by induction on Λ. - Top level: init (50 steps), then multistep_nonhalt + progress_nonhalt_cond. - Template: CounterClass2v1.v. The EXT index bookkeeping will be the bulk of the work.

New files: - check_proof.py. - scripts/inv_model.py and scripts/inv_scan.py, with output in scripts/inv_scan_out.txt (1,500 orbits, n<=30, 25,070 words, 0 failures). - Full check_proof.py run (seed 2026, 1,004 s): ALL CHECKS PASSED. Output is in scripts/check_proof_out.txt. - A: 500/500 for each TM rule. - B1: 40,000 macro steps equal to the TM. B2: 23 edge returns up to step 4e8 against the C core. - D: every epoch rule held on all random cases. - E: 49,294 orbit words, 51,879 epochs, 0 failures. - F: n <= 37, all costs 2. - G: E always reads 1.

Review pass: skeptic 1 (overnight 2026-10-10)

An independent skeptic found the proof sound and listed six minor gaps (none fatal or major). All six are closed in proof.md, and its new Review log has the details. Summary: - TL proof: reworded by cases on |S|. A pop reads a_(p-1), which lies inside S except at the |S| = 1 pop, and that pop is the epoch's last step. §7 lists the Coq invariant (i <= c, S = [] -> i < c). - Rule S: tails are now defined. U2, TR, Rule T and Rule X are stated for tails, using W_i(N) = Ep^i([1]+N). Rule S is Rule T at (2, a, [2,b]+N) plus U2, and is also a standalone 18-step lemma. - §7 Top: the progress_nonhalt_cond instance is now correct: A = nat * list nat, C '(n,W) = conf [] (3::2::W), P '(n,W) = orbit [] n W, i0 = (0,[1]). - B2: scripts/edge_scan.c is a raw-TM scan for every left-edge configuration up to step 4e8. It finds only blank, conf([],[2]), and Edge(O_n([])) for n = 0..39, all at the model's exact steps. B3 keeps spot checks against tools/sim.py. - E2 (new): adversarial test of the induction step on words built from the Inv clauses. Exhaustive at a <= 14 (93,113 words, 9,564 absorption exceptions, 306 merged), random at a <= 26 (2,000) and extreme placements (3,000): 0 failures. The sensitivity run moves a clause bound by 2, and the step then fails on every added word. Epochs longer than 2e6 macro steps run on scripts/epc.c, which agrees with the Python model 300/300. - Twin (§6.1): Eqv.v TM113.tm is this TM relabeled, started in state B. Its init is 44 steps to conf([],[2,2,1]). The budget-2 edge lemma plus the Theorem with M = [] show it never halts, and TM113.eqv then gives row 833 (1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB). Evidence H checks the init, the lemma, and a raw-TM scan from state B (n = 0..39). - Full check_proof.py run (seed 2026, 1,570 s, A–H): ALL CHECKS PASSED, output in scripts/check_proof_out_review1.txt. E2 alone with seed 11 also had 0 failures (scripts/e2_seed11_out.txt). - status.json -> CHECKPOINT_B ("proof.md ready; formalization may start").

Kill