/machines/1RB0LC_0RC0RB_1LD0RE_0LE0LF_1LA0LB_1RA---/notes.md · raw

1RB0LC_0RC0RB_1LD0RE_0LE0LF_1LA0LB_1RA---

Status: SKIPPED (2026-10-14). The twin port of upstream Sk1like_TC_v1.v Module TM1 is refuted. The machine goes back to the K42 pool (strategy direction 2).

Label: P-64 (strategy direction 1, twin ports). 740 line 64, byte for byte. Class: Skelet 1-like Class 1, K42 core.

Checks: check_twin.py gives SUMMARY PASS, 17 checks in about 20 s. Log: logs/check_twin_full.log. The symbolic executor is symexec.py.

The claimed relation

Upstream proves TM1 = 1LB0RC_0LC0LB_1RD0LE_0RE1RF_1RA0RB_1RA--- nonhalting. Line 64 mirrored (L and R swapped), called 64f below, is:

64f = 1LB0RC_0LC0LB_1RD0LE_0RE0RF_1RA0RB_1LA---
TM1 = 1LB0RC_0LC0LB_1RD0LE_0RE1RF_1RA0RB_1RA---

The state names are the same. The tables differ in exactly two entries: D1 (64f: 0RF, TM1: 1RF) and F0 (64f: 1LA, TM1: 1RA). Both start in A on the blank tape. F is entered only through D1, so the two machines agree step for step until D first reads a 1.

Line 124 is this same table renamed by TM3's renaming (A,B,C,D,E,F → D,E,A,B,C,F), so it is 64f started in TM1-state C. In the same way, TM3 is TM1 started in C. Everything below also holds for 124 against TM3, 15 Inc steps later.

Upstream's argument, in one paragraph

A configuration is toC(n, r) = 0^inf C> w^n toRC(r), with w = 0001 and r a list of digits (25 digit words, each followed by w^k). RInc is one carry pass from the left end, and Inc is one full macro step. The lemmas RInc_spec and Inc_spec prove each case by symbolic execution (es). The proof is then:

Where the exit fires, re-derived symbolically

symexec.py replays every case of RInc_spec and Inc_spec the way es does: concrete steps, shift rules with a travelling context of up to 5 cells, rotation, and the induction hypothesis at the abstract tail. All 42 obligations derive for TM1, and the 51 inr cases need no proof.

D1 fires in exactly 3 cases. In each one F reads 0:

Case TM1 result 64f result
D01 (1+c) B 0001 01 w^c r (Tp2, D01 c), 7 steps B 011001 w^c r, 5 steps
D0011101 (1+c) B 0001 0000101 w^c r (Tp2, D0000101 c), 23 steps B 0001 0011001 w^c r (Tp2, D0011001 c), 21 steps
D00101 0 · D00101 (1+c0) B 001 0001 0000101 w^c0 r (Tp1, D0000101 c0), 31 steps same with 0011001, 29 steps

So at every exit, 64f writes the word 0011001 where TM1 writes 0000101, and takes 2 fewer steps. In TM1, that word appears as the digit D0000101, or as D00001 0 · D01 after the D01 exit has gone through its caller.

The 64f map RIncF. RIncF is RInc with: - the 3 exit cases above; - a new return type Tp3 = B [0;1;1;0;0;1] w^dn toRC r', returned by D01; - D00111 n receiving Tp3 returns (D0011001 dn r', n, Tp2); - Inc receiving Tp3 with n = 1+m returns (1, D0011 m (D0011001 dn r')).

All 44 obligations of RIncF derive on 64f. The other 39 cases derive unchanged, because TM1 never fires D1 in them.

Two independent checks agree with the model: - Direct simulation (R). 2,215 random Inc steps of RIncF match direct simulation of the machine, and every exit case is hit. - Line 64 itself (S). Run unflipped from the blank tape, line 64 reaches x0 at step 1,699 and then matches 1,770 consecutive RIncF orbit states. Its F entries at steps 39,734, 841,213 and 6,436,652 fall in Inc steps 109, 607 and 1,746.

Local reconvergence, and why it is not enough

Direct re-read: the defect heals. When a later carry reaches the exit word directly, both machines produce the same tape: - TM1: D0000101 c → D001101 c in 7 steps; - 64f: D0011001 c → D001101 c in 21 steps.

This is the critic's "+12 steps per exit event": 14 extra steps on the re-read, minus the 2 saved at the exit.

Neighbour read: the defect does not heal. RInc also reads the word together with its left neighbour when that neighbour is D0011 0: - TM1: (D0011 0)(D0000101 c) → D0011_000101 c. This chain goes D0011_000101 → D0011_00101 → D0011_0101 → D0011101, and D0011101 is itself an exit case. TM1's exits sustain themselves. - 64f: (D0011 0)(D0011001 c) → D0011_011001 c. This chain goes D0011_011001 → D001111001 → D00101001, a recursive digit that carries into its right neighbour. There is no exit.

The two orbits from x0

Results of section D, on the abstract maps:

The critic's caveat is confirmed: the lockstep to 3e8 steps covered only exits 1-3.

64f further out (RIncF, scratch run): exits 10 and 11 come at Inc 2,149,311 and 43,727,620, and none follow by Inc 1e8. The digit list stays at 10-13 digits, and the counts grow into the millions. That is a counter-like regime, not a translated cycle. There is no inr up to Inc 1e8, and every case of RIncF has F reading 0. So line 64 does not halt on that stretch, which is astronomically many machine steps. This matches the K42 picture: "doesn't halt or become a TC yet".

Line 124 (same table, P-124)

The same divergence happens 15 Inc steps later (check_twin.py T, informational): - exits 1-6 at Inc 124, 622, 1,761, 207,722, 370,734 and 528,728 in both; - split at Inc 529,352 (374,704 cells); - TM3's exit 7 at Inc 529,477 is missing in 124.

So the port of TM3 to 124 fails in the same way.

Formalization route

There is none as a port. Upstream's S', Inc_Sn 1333816 and 669179 do not hold for line 64.

What carries over is an exact, case-by-case accelerator. Copy Sk1like_TC_v1.v's RD, RC, RInc and Inc, with these changes: - the 3 exit branches above; - the Tp3 constructor (prefix [0;1;1;0;0;1], state B), with one more RInc_spec arm; - D00111 and Inc handling Tp3.

The case proofs should go through with the same solve_v1 / es script. Our executor derives all 44 obligations, but this is untested in coqc. The kill file would then prove flip(tm) and conclude with flip_halts plus Perm (identity), like our kill #24.

This only accelerates the run. A nonhalting proof still needs an invariant on RIncF's counter regime, which is direction-2 (K42) work. Do not fund it as a port.

Files