P-305: 740 line 305, twin port of Sk1like_TC_v1.v TM2 / Sk1like_TC_v2.v TM1

1RB0RC_1LC0RD_0LD0LC_1RE0LA_0RA0RF_1LB--- (740 line 305, byte for byte). Skelet 1-like Class 1, K42 core.

Verdict: SKIPPED. The port does not work, against either upstream machine.

• Against TM2, the twin heals after its first 2 exits, then splits for good at its 3rd exit, at machine step 1,303,231. TM2's 4th exit (step 1,338,615) has no counterpart here.
• Against v2's TM1, it differs from the first exit on (step 49,248) and never meets it again.
• Neither upstream cycle base S' is a cycle for this machine.

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

Every number below is checked by scripts/twin_check.py. Its output is in scripts/twin_check.out.

1. Relation to the upstream machines

• All three have the same state names and start in A. There is no mirror.
• F is entered only through E1. So the three machines agree step for step until E first reads a 1, at step 49,248 in all three.
• All three reach upstream's x0 = (1, D0011 27 . D00001 8 . D001T) at step 6,039 by the same E1-free run. Upstream's init holds unchanged.

Same table as P-64 and P-124. Rename line 124 by TM3 → TM2 (A, B, C, D, E → D, E, A, B, C). The result is line 305, byte for byte (check 1). So:

• 305 is line 124's table started in 124's state C;
• in 305's names, line 124 starts in D and line 64 is the mirror started in B (canon(305, start) for B and D equals canon(64) and canon(124)).

Both other ports are already refuted (P-64 SKIPPED, P-124 STUCK). This one fails for the same reason, and much sooner.

2. Upstream's representation, in TM2's names

toC (n, r) = 0inf D> 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 D> toRC x  -->*  l <A 0    w^n toRC x'
Tp1:  l D> toRC x  -->*  l <C 001  w^n toRC x'
Tp2:  l D> toRC x  -->*  l <C 0001 w^n toRC x'

TM2's proof runs Inc 1 + 1,339,069 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. (TM2 is already at S' at Inc 669,890; upstream uses the next visit.)

3. The exit, re-derived

Exit lemma. E reads a 1 only right after D has read the 0 of a 01 that is followed by 00. Four cells are involved:

TM2  (7 steps):  D> 0 1 0 0   ->  <C 0 0 0 1
                 D0 1RE, E1 1RF, F0 1RB, B0 1LC, C1 0LC, C1 0LC, C1 0LC
305  (5 steps):  D> 0 1 0 0   ->  <C 0 1 1 0
                 D0 1RE, E1 0RF, F0 1LB, B0 1LC, C1 0LC

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

v2's TM1 does something else: after E1 0RF, its F0 0RE sends E on to the right. v2's exit continues the carry into the rest of the tape (its RInc recurses at each exit). So its exit branches are not this machine's, and v2's proof cannot be reused branch for branch.

Where E1 fires. Among all RInc branches, E1 fires in exactly three base branches:

Tp3 is a new return kind:

Tp3:  l D> toRC x  -->*  l <C 011001 w^n toRC x'

It 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')

So at every exit, 305 writes 0011001 where TM2 writes 0000101 (or 00001 0 followed by 01), and takes 2 fewer steps.

One case that upstream never needs. This machine's orbit also meets D00101 0 . D0011 n0 (first at Inc 870). Upstream's RInc has no case for it. It is a local rewrite of 25 steps that never reaches the w^n0 block:

D> 001010011 . R   -->*   <A 0 0001 0001 . R
i.e.  D00101 0 . D0011 n0 . r0   ->   (r0, 2 + n0, Tp0)

Call RInc3 / Inc3 upstream's RInc / Inc with the 3 exit branches, Tp3, its 2 handlers and this case. It is the P-124 model, renamed, plus the new case.

Checks. - Python (check 3): on every digit list of at most 3 digits with counts 0..3 (929,969 instances), TM2 meets upstream's RInc_spec, and 305 meets RInc3_spec (930,405 instances, 436 of them the new case). E1 fires only in the three branches above. The window and the 2-step delta hold on every instance. - Check 3 also verifies v2's own RInc_spec for v2's TM1 (774,144 instances), so the v2 comparison uses v2's real map. - Real machine (check 5): Inc3 predicts every configuration of line 305 for the first 3e7 steps. - Coq: scripts/P305_model.v holds RInc_spec, Inc_spec and init for line 305 in TM2's representation. It compiles with coqc 8.20 against the pinned framework in 12.8 s (scripts/P305_model.compile.txt). These are model lemmas only. There is no nonhalt, so this is not a kill.

4. Reconvergence, and where it fails

When it heals. 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

This is the critic's "+12 steps per exit": the tapes are equal again.

When it does not. If the changed digit is reached as the second digit after D0011 0, the two go different ways:

TM2:  D0011 0 . D0000101 m  ->  D0011_000101 -> D0011_00101 -> D0011_0101 -> D0011101 -> exit again
305:  D0011 0 . D0011001 m  ->  D0011_011001 -> D001111001 -> D00101001 m -> merges into its right neighbour, no exit

TM2's exits feed each other. This machine's do not.

Inc-level comparison from x0 (check 6, to 3e6 Inc steps):

The split, step by step: - Exit 3 at Inc 681 is the first 0011101 exit. It leaves its digit behind D00001 0. - At Inc 685, D00001 0 becomes D0011 0. - At Inc 690, the changed digit is read through D0011 0: TM2 makes D0011_000101, this machine makes D0011_011001. - TM2 fires exit 4 at Inc 710 from that chain. This machine has no exit there; its next ones come at Inc 2,998 and 6,036. - At Inc 870 this machine meets the new case D00101 0 . D0011 8. Upstream's map has no branch for it (RInc2 alone returns inr there).

On the list strings themselves (check 5, direct simulation for 3e7 steps), E1 fires at:

The delays are +12 and +24 steps for exits 2 and 3. TM2's exit at step 1,338,615 has no counterpart here. This matches the strategy row (equivalence-candidates.tsv S305: in sync with TM2 only to 1.3e6 steps).

The upstream cycles do not hold here: - 305 never has TM2's S' prefix up to Inc 3e6. TM2 has it at Inc 669,890 and 1,339,070. - From TM2's S'(r), TM2 returns to S'(r') in 669,180 Inc steps without reading r (24 exits per period). Inc3 reads r after 777 steps (check 7). - v2's TM1 has its own cycle base S'(r) = (406, D00111 12 . D001101 402 . D001101 391 . D00111 389 . D00101 390 . D0011 389 . r), period 518 Inc steps. Each period contains one exit (0011101). Inc3 from there reads r after 2,435 steps (check 9). - v2's Inc and Inc3 differ from Inc 99 on and are never equal again up to 3e6.

Further out (check 8): the Inc3 orbit from x0 runs to 1e8 Inc steps with no inr and no repeated (n = 1, first three digits) signature.

• It makes only 12 exits: 6 via 00101/0+00101 and 6 via 0011101, the last at Inc 23,568,781.
• At Inc 1e8 it has 12 digits, n = 23,382,679, and digit counts up to about 2.3e7.

This is a slow counter, not a translated cycle at this scale, as for lines 64 and 124.

5. What this means

• No delta proof.md. No finite run from blank reaches either upstream invariant: TM2's S' is never reached, and neither S' is a cycle of this machine.
• No formalization route as a port. Copying Sk1like_TC_v1.v Module TM2 with the new string fails three times over:
• its RInc_spec is false on the three exit branches (section 3);
• with those repaired (RInc2, the P-124 model), the orbit leaves upstream's case list at Inc 870 (inr);
• with the new case added (RInc3), it never matches S', so Inc_Sn 1339069 and the cycle step fail.

Copying Sk1like_TC_v2.v TM1 fails at its first exit, since every v2 exit branch is wrong for this machine. - A nonhalting proof needs an invariant of the Inc3 digit system: Inc3 never returns inr on this orbit. That is the K42 family problem (direction 2), shared with lines 64 and 124. - Asset for the K42 atlas. scripts/P305_model.v is a Coq-checked exact simulator for this start. Its only difference from P-124's model is the new case D00101 0 . D0011. That case is also sound for line 124 (same table) and should be added to P-124's model if its orbit ever needs it. The F entries are exactly the RInc3 calls that take the three exit branches.

Files

• scripts/twin_check.py: self-contained checker for every number above (--quick, --long N, --n6 N).
• scripts/twin_check.out: output of twin_check.py --long 1e8.
• scripts/P305_model.v: Coq model lemmas (RInc_spec, Inc_spec, init) for line 305.
• scripts/P305_model.compile.txt: its coqc run.