/machines/1RB0LF_1RC1RB_0RD0RC_1LE1LF_1LD---_0LB1LA/notes.md · raw

1RB0LF_1RC1RB_0RD0RC_1LE1LF_1LD---_0LB1LA

Status: STUCK (parked 2026-10-11). Twin port P-500 of upstream SBCv9.v TM2 (HALT) refuted 2026-10-14: TM2's halting event is not one for #37 (see the last section). Earlier: follow done 2026-10-10, real orbit in sync to phase 1,857 with no halt. Class guess (agent / Dennis): Sync bouncer counter: a binary counter on the left, an eroding 1-block timer on the right, and a doubling reset / _ Spreadsheet notes / Discord thread: Results row 919, "Sync bouncer counter", with no status, notes or done-by. The Discarded tab (row 50) says "Was mentioned but no work done". It is still in the 778 list (Oct 7, line 530). Not claimed. It is on mxdys's UBRRBA_TODO list (2026-08-24, data/discord/2026-08-24_mxdys_ubrrba_86.txt line 46: "easy to accelerate by UBRRBA"). That is a technique hint, not a claim; our kill #4 came from the same list. There are no sheet links. Not on dyuan01's longitudinal list. Pool #37 in reports/targeting.md. Viewer: https://bbchallenge.org/1RB0LF_1RC1RB_0RD0RC_1LE1LF_1LD---_0LB1LA

Transitions: A0 1RB, A1 0LF | B0 1RC, B1 1RB | C0 0RD, C1 0RC | D0 1LE, D1 1LF | E0 1LD, E1 halt | F0 0LB, F1 1LA. The only halt is E reading 1. E is entered only by D0 -> 1LE, and E/D walk left over zeros, filling them in.

Observation

Candidate rules

All rules were checked by direct simulation on random instances. Scripts: scripts/validate_rules.py (seeds 7 and 11, logs in work/validate_rules_seed*.log) and scripts/validate_visit.py (work/validate_visit_2.5e9.log).

rule from to steps cases check
V visit 0^inf L 1^m 0^g C> 0^inf 0^inf inc(L) 1^(m+d) 0^(g+4) C> 0^inf 6m+2g+c(L) m>=4, g even; (inc(L), d) depend on L only every visit to 2.5e9, real L, random m' (same parity) and g' (both residues mod 4): 54,248/54,248
Inc carry depth of visit k v2(k+c)+1 digits one c per phase 27,084/27,124 (40 = digit migration)
R0 0^inf L0 0 1^n 0^g C> 0^inf 0^inf L0 1^(n-1) 0^(g+4) C> 0^inf 6n+2g-10 n even >=4, g even, any L0 600/600
R1s L0 1 0 00 1 1^n 0^g C> L0 1 1 00 0 1^(n-2) 0^(g+4) C> 6n+2g+10 phase-10 layout, any L0 600/600
R1d L0 1 0 00 00 00 1 1^n 0^g C> L0 1 0 00 11 00 0 1^(n-2) 0^(g+4) C> 6n+2g+14 phase-9 layout, any L0 600/600
R reset 0^inf L0 0 1^2 0^g C> 0^inf 0^inf L0 1^(g+6) C> 0^inf g = 0 mod 4, any L0 600 random + 36 on the 12 real resets
P pad 0^inf X 1^n 0^g C> 0^inf 0^inf X 1^(n-1) <F 1^(g+3) 0^inf g+4 g even 400/400
H same, g odd halt 400 random + 5,425 on real L
S stripe L 1^(2k+1) <F R L <A 1 (01)^k R 2k+1 400/400
Z zigzag 1^a C> (01)^k 1^b 0^inf 1^(a+2k-1) C> 1^(b+1) 0^inf 10k-5 k>=1 400/400

What is NOT ruled yet: - the grammar K of counter words L, meaning which digit/filler layouts occur and how inc and the reset act on a general layout; - the absorption visits early in a phase; - why the reset visit always has bit 0 = 0.

Template check: no solved machine is within 3 transitions. The nearest are CTLv1, RWL_mod and CPS_LRU decider machines at 4. SBCv7 TM4 (also the base of our kill #4) and SBCv11 match at class level only. Their counter lemmas (BC.Mul2 on fixed 4-cell digits d0/d1) do not fit 1- or 2-cell digits with phase-dependent fillers.

Cryptid check (ground rule 6): not cryptid-like. The counter is a plain binary +1 (ruler sequence), and the timer arithmetic is linear (n -> n-2, g -> g+4, reset n' = g+6). No halting decision depends on pseudo-random arithmetic. The open question is structural: closure of the layout grammar and the sync.

Checkpoint A (Dennis)

Informal proof

Not started (waits for Checkpoint A).

Formalization log

Not started.

Outcome

Open (CHECKPOINT_A after the follow stage, see that section; recommended: park).

Decision (2026-10-10)

Question: #37's visit, reset and halt rules are exact. What is open is the counter-word grammar K (its closure under inc and reset) and the reason every reset lands on bit 0 = 0. Spend one deepen stage pinning K, or park #37? Answer: deepen (Fund one ~2 h deepen stage on the counter grammar K). Dennis: go with all recommendations (2026-10-10).

Funded stage (2026-10-10, deepen)

Scope (decision deepen): dump L at every visit to 1.2e10, write K, check inc and the reset on random members, derive the bit-0 sync. Scripts: scripts/deepen/ (C tracker lowend.c, Python lib37.py); logs: work/deepen/.

Data. scripts/visitpairs 1.2e10 1 -> work/deepen/allvisits_1.2e10.txt: all 57,448 visits, 14 resets, no halt (65 s). Ruler check on it: 57,378/57,431 visits (work/deepen/ruler_1.2e10.txt).

What changed in the picture. Bit 0 is not a cell of L. It is the parity of the block: m odd means the block's first cell is bit 0 = 1. The block's left end oscillates between two fixed cells b-1, b for the whole phase; only its right end erodes. Notation: z = final gap of L (zeros between L's last 1 and the block), r = L's bottom (last) 1-run. - K (closed). K = words whose 1-runs all have length >= 2. All 57,448 real words are in K. Random closure (validate_K.py 21 300 60): 18,000/18,000 visits stay in K, every visit returns with pad g+4, no halt. Within a phase nothing ever halts: 1,000 fully random binary words x 60 visits (randiter2.py 2 1000 60 30) and 300 K-words x 100 visits (randiter.py 1 300 100), 0 halts. The layout of the high digits (drifting long runs, gaps that shrink and merge) needs no description for this: K is enough for the visit rule. - D (block change, exact). For L in K: d = -1 if m is even, d = -3 if m is odd, as long as z >= 2; if z = 1 the bottom run merges into the block and d = r-1. Real: 57,433/57,433 transitions (7 merges, all early in a phase). Random: 18,000/18,000. Without K (single 1s allowed) d takes other values (dtest.py 3 4000 40: d in 2..12 on 503 of 1,890 odd visits with z >= 2). - S (sync invariant). m mod 4 in {1,2} at every visit with g > 0: real 57,433/57,433. By D it is preserved by every visit with z >= 2. A merge keeps it only if r = 1,2 (mod 4) at an odd visit or r = 0,1 (mod 4) at an even one. So off-sync can only enter through a merge. - P (low-end lemma). If z >= 3 at an even visit, then at the next even visit z >= 4 when it was 3, and z = 3 when it was >= 4 (bit 1 of the counter). So z never drops to 1 or 2 again and no merge happens for the rest of the phase. Real 28,698/28,698 even-visit pairs; random 8,688/8,688. Micro-cause: at the odd visit F meets z-1 zeros; z-1 = 3 extends r by one cell, z-1 >= 4 builds a new 11 digit, z-1 = 2 passes the carry into r; every case leaves z >= 3. Phase test (phasetest.py 11 800 400 8): starts with z >= 3: 583/583 runs x 400 visits with no mod-4 violation; starts with z in {1,2}: 117 of 217 violate, always within the first 4 visits. - R (reset). z at the new phase start = z at the reset visit minus 1 (13/13 non-trivial resets). Phase arithmetic: n' = 4 x visits + 2 in all 13 phases, and visits = n/2 when no merge happens. Forced resets on real mid-phase words (forcereset.py 1): z_reset >= 4 gives a synced next phase end in every sampled class (532/532 runs); z_reset = 3 is safe or fatal depending on r (R1/5: always m=2; R3 and 3: always m=3; R0, R2, 2, 4 mixed). - Sync, derived for the steady class. Class Sigma: n = 6 (mod 8), z = 3 at phase start, and the bottom run long enough that z alternates exactly 3/4. Then visits = n/2 = 3 (mod 4), the reset is at an offset = 2 (mod 4), so z_reset = 4, z' = 3, and n' = 4 visits + 2 = 6 (mod 8) again. The real run has been in Sigma since phase 11 (k = 6,697): n+2 = 1681 x 2^j (13,448 ... 107,584), z_start = 3 and z_reset = 4 in phases 11-14, bottom run 26..80, z_even exactly {3,4}. Earlier phases left Sigma twice (phase 7 ended with z_reset = 8 while the bottom run was a 2-run digit; phase 9 had z_reset = 3) and came back through benign merges (r = 2, and 2 then 5 in phase 4). - Random multi-phase tests (steady.py, multiphase.py): Sigma with bottom run >= 3: 249/250 runs stay in sync over 5 phases (1,317 phase ends); the one failure starts with a 4-run that shrinks to an 11 digit. Sigma with a bottom 11 digit: 63/150 runs go off-sync (47 halt). Outside Sigma: 120 of 238 runs go off-sync (multiphase_seed1.log).

What is still open (one lemma). B: in the real orbit the bottom run never again becomes an 11 digit in a position that is erased at a bad time (a bottom 2-run is erased by a carry and makes z = 7/8, which shifts the 3/4 pattern by 2 visits and makes z_reset = 3). Its length moves only at carries of level >= 2 (left end: -1 at a gap of 3 or >= 4 above it, +1 at an A arrival, +big at merges with the run above; data 30, 28, 27, 31 at phase starts and up to 80 in phase 15). So B is a statement about the high digits of K, which this stage did not describe: K as "runs >= 2" is closed but too coarse to prove B (random upper words do break it, 1/250). Nothing here is arithmetic beyond n mod 8, so it is not a cryptid, and the stop rule ("depends on block-length arithmetic in a non-regular way") did not fire. But the sync is not derived for every phase, so proof.md is not next yet.

Decision (2026-10-10, auto-applied)

Question: #37's sync now rests on one open lemma B (its bottom counter run never again becomes an erasable 11 digit): fund a second deepen round on B, or park #37? Answer: deepen2 (Fund a second ~2 h deepen round on lemma B). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was at lunch). Override any time.

Funded stage (2026-10-10, deepen2)

Scope (decision deepen2): settle lemma B (the bottom run never again becomes an erasable 11 digit) by tracking the bottom run and the gap above it, and write the grammar of the high digits that B needs. Scripts: scripts/deepen2/. Logs: work/deepen2/. Phase numbers are real phases (phase 11 starts at step 150,742,757). jump_160.log counts from phase 11 as index 0, so real phase = index + 11.

1. Inside a phase the counter is a binary counter on fixed cells (bitcells.py on the 1.2e10 dump, work/deepen2/bitcells_1.2e10.log). After a short settling, each carry level toggles a fixed group of 1 or 2 cells. - Phase 13 (n = 53,790): bit 1 = cell -47 (13,447 flips), bit 2 = -78 (6,722), bit 3 = -81 (3,361), then -104, -107, -126, -129, -134, {-138,-137}, {-142,-141}, ... - Only L changes at the odd-m visits. The counter value at every steady phase start is N0 = 3. - The only other changes are one-time migration fills: a carry fills a gap cell instead of carrying. In phase 14, for example, -79, -80, -105 and -106 are filled before bit 2 settles at -127. - So the bottom run is filler between bit 2 (its left end) and bit 1 (its right end).

2. Exact accelerators. - Visit level, fastphase.c. Each visit runs on the real TM with the block replaced by 1^(8 + m mod 4) (rule V). The true m is carried through d, and the reset uses rule R. It matches the real TM dump on 50,752/50,752 visits from k = 6,697 to 57,448, including 3 resets (cmpdump_6697_57448.log). - Phase level, jumpsim.py. It memoises a run of 2^lam - 1 units (each of carry level <= lam) on the exact contents of every cell the run reads, so a replay is sound by construction. It learns the alignment from carry depths. - Agreement. jumpsim reproduces all 15 phase-start layouts that were simulated exactly (phases 12-26, cmplayout_jump_vs_exact.log). It follows the real orbit to phase 171 (n ~ 9.8e51) in about 2 minutes.

3. B is false as stated, and the orbit survives anyway (jump_160.log). - From phase 15 on, the bottom run erodes by exactly 1 cell per phase: 78, 77, ..., 3, 2. Its right end follows the block (z' = z-1 at each reset) and its left end (bit 2) stays put. The low layout .3 r .3 14 .3 12 .3 3 .3 is frozen from phase 19. - It becomes an 11 digit at phase 91, and again at phase 119 (after the 14 and 12 runs are used up, merges give 24, then 77). - Both times the same 3-phase excursion follows: - Phase A (r = 2) ends with z_reset = 8. - Phase B starts with z = 7, the next run is the bottom run, and it ends with z_reset = 3. - Phase C starts with z = 2. A fresh 11 digit merges once (d = +1, which keeps m mod 4 in {1,2}), and the phase ends with z_reset = 4. - From phase D the run is back in the steady class, with bottom run = next run - 2. - To phase 171: 2 excursions, no off-sync, and z_start 3 / z_reset 4 in every other phase. - The merge adds one visit, so n+2 = 1681 x 2^j becomes 8 x (1681 x 2^83 + 1) after the first excursion and changes again after the second. Each excursion adds one bit to the final counter value, and that bit rises one level per phase through the layout.

4. When the excursion is safe (excursion.py, which starts from the real phase-119 configuration). - Next-run length 70..81: 12/12 benign, the same pattern for every residue mod 4 (excursion_vary1_ph108.log). - Random runs above, separated by 000 (bottom 11 digit, 6 random runs): - lengths 2..40: 60/60 benign over 4 phases; - lengths 3..12: 60/60 benign over 4 phases; - lengths 2..8 over 16 phases: 9/40 go off-sync (excursion_rand_seed3_a2-8_16ph.log). - Every failure has a run of 3 or 4 becoming the bottom run during or right after an excursion. Excursions then overlap (z 2 > 8, or z 3 > 7 > 6), and off-sync means a halt on the next visit (rule H). - So the true replacement for B is B': no run of length <= 4 becomes the bottom run around an excursion, unless it merges first.

5. Where B' stands. - At phase 171 the layout has 3,616 cells and 78 runs. The lowest 18 runs are separated by exactly 000, with irregular lengths: 46 93 177 112 69 176 84 247 276 21 17 41 65 34 375 3 46 ... - Further up, the gaps are 2, 4, 7, 11, 14, 15, 18 and 23. That region is where the rising bits of the final counter value write the layout. - A 3-run sits 16 runs above the bottom. It reaches the bottom roughly 2,000 phases from now, unless merges absorb it first. Merges do happen after excursions: 75+17 -> 93 and 58+33 -> 93 around phases 123-126. - So B' depends on a layout that the history of excursions writes (each excursion changes the final counter value, which changes the layout written above). I found no regular grammar for it in this stage. This meets the decision's stop rule, so the status is STUCK. - It is not a cryptid as far as tested: no dependence on run-length residues, and the counter arithmetic is powers of two plus sparse bits. But a halt far out (a short run reaching the bottom at an excursion) is not excluded.

Still open. - Whether the 3-run, or any run of length <= 4, ever reaches the bottom at an excursion in the real orbit. - A C port of jumpsim with hashed memo keys (the Python version needs about 1 s per phase at phase 160 and grows with the level count) could follow the real orbit through the next excursions (about phases 205-2,200). That would settle it empirically: either a halting candidate with an explicit phase, or evidence for a maturation rule. - A proof would need a phase-of-phases induction over that layout grammar. No busycoq template is near.

Decision (2026-10-10, auto-applied, round 3)

Question: #37's sync now hinges on whether a short run ever reaches the bottom during an excursion: port the jump simulator to C and follow the real orbit through the next excursions, or park #37? Answer: follow (Port the jump simulator to C and follow the real orbit (~2 h)). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was away). Override any time.

Funded stage (2026-10-10, follow)

Scope (decision follow): port the jump simulator to C, re-check it, follow the real orbit from phase 171 until the 3-run 16 runs up reaches the bottom (about 2,000 phases) or the cost explodes. Scripts: scripts/follow/. Logs: work/follow/. Phase numbers are real phases; the simulator files count from phase 11 as index 0, so real phase = index + 11.

1. The C port is exact against everything we have (work/follow/cmp_c_vs_py_160.log, validate_*_seed7.log, check_cycles_seed1.log). - jumpsim.c is a line-by-line port of jumpsim.py, with GMP integers and m mod 4 added to the memo key (strictly more conservative). On the real orbit from phase 11 it gives the same log as Python for all 160 phases, every field including exact_steps, and the same 160 layouts. It also matches the 13 exactly simulated layouts. - jumpsim2.c adds fast paths: an 8-cell macro table, the F/A sweep over a 1-run, three zigzag cycles (1 C>0 1 0 1, C>1 0 1, 0 C>0 1; each one is 10 steps and shifts by 2), and C or B crossing a 1-run. A brute-force check on random surroundings passes 3,000/3,000 for each of the four rules. On the same 160 phases its layouts and phase fields equal Python's. - Random instances use real layouts with the lowest 3-8 runs rewritten in three kinds: excursion-style, K-words with gaps 2-6, and words with single 1s. Each C binary was compared with two references: - the Python jumpsim: 90/90 instances (248 phases, 37 of them ending off-sync), all agreeing; - the exact visit-level fastphase.c: 90/90 instances (250 phases, 41 ending off-sync), all agreeing. - Speed: index 160 takes 0.23 s, against about 2 minutes in Python. At index 1,800 a phase takes 0.9 s; the counter word is then 146,000 cells and the cost grows like (word length) x (levels).

2. Real orbit followed to the start of phase 1,857 (index 0..1,845; real.log + real2.log, runs per phase in real_runs.txt + real2_runs.txt, resumable checkpoint ckpt_follow_end.txt). n is about 2^1860 there. There was no off-sync and no halt. - Excursions (bottom run 2) happened at phases 91, 119, 215 and 487. Each was the same benign 3-phase pattern: z_reset 8; then z 7 > 3; then z 2 with one merge. The run that became the bottom had 14, 77, 93 and 700 cells. - The 3-run from the decision never reached the bottom. A merge wave absorbed it at phases 231-233: 412 .2 4 .3 46 -> 418 .4 45 .2 38 -> 418 .3 86. - Excursions are getting rarer. The bottom run after each merge cascade was 24, 93, 269 and 2,824, so the gaps between excursions were 28, 96, 272 and about 2,834 phases. The next real excursion is due at phase 3,321.

3. What happens between excursions (frozen.py -> frozen_real_1846.log; Fig 5 = img/follow_lowruns_real.png). - Erosion. The bottom run loses exactly 1 cell per phase and the gap above it stays 3: 1,777 of 1,779 steady phase pairs. The 2 exceptions are phases 14-15, before the steady class. - Wave and frozen region. After each excursion a wave climbs from the bottom at about 0.5 runs per phase. - Where it passes, a gap of 3 becomes 2 and the two runs merge in the next phase. The bottom run absorbs runs this way (698 -> 975 -> 1,017 -> 1,127 -> 1,547 -> 2,533 -> 2,824 at phases 490-499). Runs further up merge in pairs or triples (23 + 77 -> 102, ...). - The wave also writes some new short runs. - Below the wave front nothing changes until the next excursion. In Fig 5 these frozen runs are the vertical stripes, and the waves are the diagonal bands. - Short runs. Runs of 1-4 cells do occur above the bottom. Since phase 223 the lowest one has sat at index 5 or higher; since phase 521 there has been a 2-run at index 11. So far every wave has absorbed the short runs it met.

4. Fast-forward and the next three excursions (ffwd.py, work/follow/ffwd/). - The method. The runs below the wave front are frozen and the bottom run only erodes. So a real layout with its bottom run cut to 4 cells should act, in its low region, like the real layout (r - 4) phases later. - Check against the past. - Donors at phases 311 and 411, cut to 4 or 5 cells, reproduce the real excursion at phase 487 and its cascade exactly: the lowest 12 and 14 runs agree over 45 of 45 phases each (d300_r4.txt, d400_r5.txt). - Donors whose wave front was still low diverge exactly where the cascade reaches runs that were not yet frozen. Donor phase 261 first differs at run index 13, at phase 496. Donors at phases 106 and 161 also diverge. - The next excursion, at phase 3,321. - Donors at phases 811, 1,011 and 1,207 give identical lowest 30 runs over 70 phases. - a1 = 555 becomes the bottom and the 3-phase pattern is benign. - The cascade merges 553 + 988 -> 1,542 (the new bottom), and 22 + 77 -> 102 (the new a1). - The 2-run at index 11 is absorbed at phase 3,336 (2 .2 41 -> 45). - Chained predictions. These are only valid in the region below the simulated wave front, so they are weaker evidence. - Phase 4,866: a1 = 102, benign. New bottom 300, a1 = 1,052. - Phase 5,172: a1 = 1,052, benign. New bottom 2,497, a1 = 3,596. - The next one after that is due at about phase 7,675. - The trend. Bottom and a1 after each cascade: (24, 77), (93, 93), (269, 700), (2,824, 555), then predicted (1,542, 102), (300, 1,052), (2,497, 3,596). In all 7 cascades both are merge products (at least 6 cells). Low-region runs keep growing.

What this settles, and what it does not. - Settled empirically: - The real orbit stays in sync to phase 1,857 (n ~ 2^1860). - The specific 3-run never reaches the bottom. - The next excursion (phase 3,321) is predicted benign by an exact simulation of the frozen low region. That prediction was confirmed on the past excursion at phase 487. - Maturation rule candidate M: - After every excursion, the cascade's first merges produce both the new bottom and the new a1. - So a1 >= 6 at the next excursion, which is then benign by the excursion rule (next run >= 5: 12/12 + 120/120 in deepen2). - Evidence: 4 real and 3 predicted cascades. - Open: - Why the wave merges at index 1. It is driven by run-length parities (F or A arrives at a gap, so 00 is filled or a digit is set), so it is probably a finite-state rule on run residues. Not derived. - A proof. It would need the visit rule, the fixed-cell phase rule, the wave rule on run words, and M as an invariant, each over unbounded nested structure. No busycoq template is close. - Not a cryptid as tested. The irregular run lengths come from history, but the safety comes from merging (runs grow), not from coincidences of residues. - Cost. It did not explode, but it grows (about 0.9 s per phase at phase 1,857). Confirming phase 3,321 on the real orbit would take about 1 h of one light C process from ckpt_follow_end.txt:

scripts/follow/jumpsim2 @work/follow/ckpt_follow_end.txt 0 0 1500 <lay> <runs> 1846 20

Decision (2026-10-11)

Question: #37 stays in sync to phase 1,857, and its next excursion (phase 3,321) is predicted benign: park it, spend one round deriving the merge-wave rule, or first confirm phase 3,321 on the real orbit? Answer: park (Park #37 behind the other machines). Dennis: go with recommendations (2026-10-11).

Twin port P-500 (2026-10-14, strategy direction 1): refuted

Label: P-500 (740 line 500, byte for byte). Scripts: scripts/port/. Logs: work/port/. One-pass check: python3 -B scripts/port/check_twin.py work/follow/real_lay.txt (about 6 min, work/port/check_twin.log).

Target. SBCv9.v Module TM2, 1RB0RF_0LC---_1LD1LC_0LE0LD_1RE1RF_0RC1RA, a HALT proof (upstream commit 457869d, 2026-02-15; identical in vendor 0940bb9). It proves halts tm c0 by init (c0 to cfgL' 11 5 ([1;0]*>0inf)), then msteps 15000 evaluated by native_compute, then 13,297 concrete steps with a and b generalized.

Relation (exact, at the table level). Mirror #37 and rename its states A, B, C, D, E, F to TM2's A, C, D, E, G, F (G is #37's E). The result is TM2 except at two places:

where TM2 #37 (mirrored)
A reads 0 A0 1RB, B0 0LC, C1 1LC: 3 steps; halts if B reads 1 A0 1LC: 1 step, same tape
E walks over 0s E0 1RE (one state) E0 1RG, G0 1RE (alternating); G1 halts

TM2's run in its own representation. LC a b = 0inf 1^a (10)^b (the timer) and a concrete counter word r. scripts/port/tm2_msteps.py transcribes mstep, rest and RIncs exactly. - The run stops after 12,417 macro steps (so msteps 15000 returns that configuration), with 374 overflows (LOv). It ends in cfgR' a b r with a of 373 bits, b of 378 bits and r of 12,511 cells. - That is 16 macro steps after the 374th overflow, about 0.6% into the phase. - From there TM2 halts at exactly step 13,297 (B reads 1 at cell 12,508 of r), never reading LC a b. This reproduces upstream's stepn' 13297 (check T5).

#37 follows that run exactly. - After overflow j, TM2's b is n - 1 for #37's phase j+1 (n + 3 at absorption phases). Its r is the reversed left word L of the follow-stage START line j - 9. - All 220 recorded counter words are equal, the last one at the start of phase 370 (check T4). cmp_phases2.py (work/port/cmp_tm2_vs_500_layouts.log) compares the 202 of them whose paired n is also recorded, b included. So upstream's formally checked macro run and our C follow simulator agree, through the excursions at phases 91, 119 and 215. - TM2's exit therefore falls early in #37's phase 375. The follow stage ran #37 through phase 375 to phase 1,857 with no halt.

Exit branch, re-derived on the upstream representation (a and b kept symbolic). - Start from TM2's final cfgR' a b r. Mirrored #37 makes the A0 turn where TM2's B would read the 1, then carries on. - After 72,652 steps it reads LC a b for the first time, in state D, with 0 1 1 to its right. That is LC a b {{{(hL',L)}}} r'', TM2's own cfgL' a b r'', and TM2's next macro rule there would be LIncs (exit_window.py; check T5). - So TM2's halting event is not an exit for #37. #37 goes back into the upstream invariant and continues the phase.

Left-side lemmas on #37 (lemma_transfer.py, a in 0..23, b in 0..7; check T6). - LInc, LRst_101 and LRst_11 hold for #37 exactly when a is odd: for even a, the timer sweep's E-run is odd and #37 halts. LOv holds for every a. - Along the orbit a = 3 (mod 4) at every configuration: a = 11 at init, 3 after each overflow, and +4 per increment. - So in this representation the whole timer side is parity-safe. #37 can halt only on the counter side: in a concrete R-sweep, or in a counter-word segment with an odd E-run.

Verdict. The halting event differs, so there is no halting port: TM2 halts on a guard #37 does not have, and #37 continues inside the same representation. Status stays STUCK (parked). Nothing new needs a decision from Dennis.

What it leaves for #37. - TM2's representation is an exact accelerator for #37. Its Coq lemmas could be re-proved for #37 under "a odd" with the same tactics. - It shrinks the open question to the counter word r. A nonhalt proof still needs the counter-side invariant (lemma B' / rule M of the follow stage). A halting proof would need a counter-side odd E-run later than phase 1,857.