P-124: 740 line 124, twin port of Sk1like_TC_v1.v TM3

1RB0LC_0RC0RF_1RD0RE_1LE0RA_0LA0LE_1LD--- (778 line 131). Skelet 1-like Class 1, K42 core.

Verdict: STUCK. The port does not work. The twin reconverges after its first 5 exits, which is all the 3e8-step evidence saw. At the 6th exit (Inc 528728, at least 1.0e11 steps) it splits from TM3 for good. Upstream's cycle base S' is never reached and is not a cycle for this machine.

What survives is an exact digit-level model of this machine, checked by Coq. It is the input direction 2 (K42) needs.

All numbers below are checked by scripts/twin_check.py (output: scripts/twin_check.out).

1. Relation to the upstream machine

• Same state names, same start state A, no mirror, no renaming.
• F is entered only by B1, so the two machines agree until the first time B reads a 1.
• Both reach upstream's x0 = (1, D0011 15 . D001T) at step 1351 by the same run, so upstream's init holds unchanged.
• First B1 at step 40898 in both.

2. Upstream's representation (short)

toC (n, r) = 0inf A> w^n toRC r        w = 0001
toRC (RC_S d n r) = d w^n toRC r       toRC (RC_O D001T) = 001 0inf

RInc rewrites the digit list from the left. Each call returns one of:

Tp0:  l A> toRC x  -->*  l <C 0    w^n toRC x'
Tp1:  l A> toRC x  -->*  l <E 001  w^n toRC x'
Tp2:  l A> toRC x  -->*  l <E 0001 w^n toRC x'

Inc wraps one RInc call into toC x -->+ toC x'. TM3's proof runs Inc 1 + 1,333,831 times from x0 to

S'(r) = (1, D0011 33 . D00001 416889 . D00001 0 . D0000101 31217 . r)

and then shows S'(r) -->+ S'(r') in 1 + 669,179 steps for every r.

3. The exit, re-derived

Exit lemma. B reads a 1 only right after A has read the 0 of a 01 that is followed by 00. The four cells involved:

TM3  (7 steps):  A> 0 1 0 0   ->  <E 0 0 0 1
                 A0 1RB, B1 1RF, F0 1RD, D0 1LE, E1 0LE, E1 0LE, E1 0LE
here (5 steps):  A> 0 1 0 0   ->  <E 0 1 1 0
                 A0 1RB, B1 0RF, F0 1LD, D0 1LE, E1 0LE

Both runs end in E, one cell left of the window, with the same tape to the left.

Where it fires. Among all RInc branches, this happens in exactly three base branches:

Here Tp3 is a new return kind:

Tp3:  l A> toRC x  -->*  l <E 011001 w^n toRC x'

The rest of each branch, including the callers' handlers (D00111, Inc), never reads the window again. So the final tape here is TM3's final tape with 0001 replaced by 0110, two steps sooner. In digit terms:

TM3:   ... 0000101 w^m ...   (D0000101 m, or D00001 0 . D01 m)
here:  ... 0011001 w^m ...   (D0011001 m)

The new Tp3 needs two handlers:

D00111 (1+n) . [Tp3 (x', dn)]  ->  (D0011001 dn . x', 1+n, Tp2)
Inc (1+n, ...) on Tp3 (x', dn)  ->  (1, D0011 n . D0011001 dn . x')

Checks. - Python: on every digit list of at most 3 digits with counts 0..3 (929,969 instances), TM3 meets upstream's RInc_spec and this machine meets the modified one, RInc2_spec. B1 fires only in the three branches above, and the window/step delta holds on every instance. - On the real machine, Inc2 predicts every configuration for the first 3e7 steps (4,467 Inc steps). Exits fall at steps 40898, 842457 and 6437976; TM3's are at 40898, 842445 and 6437952. - Coq: scripts/P124_model.v holds upstream's header with the 6 edits above, plus TM3's module with the new TM string and one extra proof bullet in each spec. RInc_spec, Inc_spec and init for this machine compile with coqc 8.20 against the pinned framework in 11 s, so the model is exact. These are model lemmas only: there is no nonhalt, so it is not a kill.

4. Reconvergence, and where it fails

When it reconverges. If RInc next reaches the changed digit as the leading digit, both versions go to the same digit:

D0000101 m  ->  D001101 m
D0011001 m  ->  D001101 m

That is the bounded-delay reconvergence the strategy data saw: +12 steps per exit, with record tapes equal again.

When it does not. If the changed digit is reached as the second digit after D0011 0 (branch 0011/0+X), the two versions go different ways:

TM3:   D0011 0 . D0000101 m  ->  D0011_000101 m -> D0011_00101 -> D0011_0101 -> D0011101 m -> exit again
here:  D0011 0 . D0011001 m  ->  D0011_011001 m -> D001111001 -> D00101001 m -> merge (2+n+dn, Tp0), no exit

TM3's exits feed each other: its S' loop has 24 exits per period (18 via 0011101, 6 via 00101/0+00101). This machine's exits do not.

Inc-level comparison from x0:

Exits 1-3 are the three seen below 3e8 steps. Counting only A's pass over w^n, a lower bound of 4n steps per Inc puts exit 4 past 3.4e10 steps and exit 6 past 1.0e11.

Consequences: - TM3 is at S' at Inc 1333832, 2003012, 2672192, ... This machine never has the S' prefix up to Inc 3e6. - S' is not a cycle here. From S'(r), TM3's Inc returns to S'(r') after 669180 steps without reading r. This machine's Inc2 reads r after 777 steps. - The Inc2 orbit from x0 runs to 1e9 Inc steps (check 8, twin_check_long1e9.out) with no inr and no repeated signature (n = 1, first three digits). It makes only 11 exits (1 01, 7 00101, 3 0011101), with 9-13 digits and counts up to about 3e8. It is a slow counter, not a translated cycle at this scale. This matches mxdys's note on K42 member line 496 ("~10^64 tape size and doesn't halt or become a TC yet").

5. What this means

• No delta proof.md: no finite run from blank reaches upstream's invariant, and upstream's cycle does not hold for this machine.
• A nonhalting proof needs an invariant of the Inc2 digit system: Inc2 never returns inr on this orbit. That is the K42 family problem (direction 2).
• The Coq-checked Inc2 model is a ready, exact digit-level simulator for that work. For the atlas, the F entries are exactly the RInc2 calls that take the three exit branches.
• Pair (line 64). In TM3's names, 64 is the same table with B1 = 0RF but F0 = 1RD. Its exit returns in state C, not E (A> 0100 -> <C ...), so its model changes in more places and needs its own Inc-level comparison. Expect the same kind of break.

Files

• scripts/twin_check.py: self-contained checker for every number in this file (--quick, --long N).
• scripts/twin_check.out: output of twin_check.py --long 1e8.
• scripts/twin_check_long1e9.out: check 8 alone, run to 1e9 Inc steps.
• scripts/P124_model.v: Coq model lemmas (RInc_spec, Inc_spec, init) for this machine.