The ten escape rules

Every variant has its own rule for an escape with a positive exponent m after the 01. It applies in all three F contexts (01^m, 00101^0 00101^m, 0011101^m) and also when the context is reached by recursion. The rules below were measured from n = 5 and 9 and from m = 1 to 6 (d01rule.py, ruleprobe.py); the results are linear in n and m.

For comparison, mxdys's proved variant (1RF, 1RB) has the rule w^n 01 w^m r → w^1 0011 w^(n-1) 00001 01 w^(m-1) r. It keeps the 01, and only adds a digit in front of it.

Read plainly, each rule puts the escaped 01 back into the counter as one of the counter's own digits. Which digit depends on the class: 00101, 001, 00111, 001101, 001111, 00001 or 0011001, which is the same as choosing a phase of the five-phase digit cycle. After that the counter simply carries on.

(a) Do the F entries follow a recurrence?

Partly. Escapes at the very front of the tape (depth 0, context 00101^0 00101^x) happen at front numbers

n = 100·25^k − 11   or   n = 400·25^k − 11
(n = 89, 389, 2489, 9989, 62489, 249989, 1562489)

FPATTERN_LINE

That is a base-5 regularity. It matches the 5^k-Inc acceleration that mxdys uses in Sk1like_TC_v2.v (RIncs_spec', n → n + dn + 5^k).

Three things show no recurrence that we could find: - the escape's own exponent x; - the deeper exponents; - the escapes at depth ≥ 1, and the contexts 01^m and 0011101^m.

For example, line 260 has three escapes in a row at n = 62489, with x = 65525, 51913 and 35623. The gaps between F entries, counted in Incs, are irregular in every line (tables below). An F entry is simply the moment when a digit's exponent reaches 0 next to the right neighbour, so its timing inherits the full mixed-radix arithmetic of the counter.

(b) Can E ever read the 11 that leads to a halt?

Halting needs F to read a 1. F is entered only from E reading a 1. E reads a 1 only while the head is moving right, at the 1 of a 01. E is entered from D, or straight from F in classes D and E. When D is entered moving left, it always hands E a cell that was just written 0. So:

1. The escape is safe when the 01 is followed by w (exponent m ≥ 1, or m ≥ 2 in classes I and J). F then reads the first 0 of w = 0001. - We checked every holdout variant, all four contexts, m = 1 to 6, and every one of mxdys's 25 digits as the next digit (closure.py). None of these halts. - In classes A, B, C, E, F, G and H every result parses back into mxdys's 25 digits. - Class D leaves the language when the digit after the escape is 001, 0010101 or 001011 (mxdys's Tp1 digits). It produces a digit 000001; we found no immediate halt. This does happen: on lines 306, 361, 587 and 673 the first escape (Inc 127-140) meets the tape's end digit 001. The new digit was present at 24 parsed Inc boundaries, and the runs went on normally. - Classes I and J do the same at m = 1 for eight next digits, and halt at m = 1 when the next digit is 001011.
2. The dangerous case is a "glued" escape: exponent m = 0, so the 01 sits directly against the next digit. Per class: - I and J (lines 86 121 405 285 421 713): the machine halts in the same Inc whenever the glued digit starts with 0011. That is 16 of the 25 digits, since the tape 01 0011 lets F → D → E → F read 11. - B (lines 263 266 67 321 664 688): a glued 0011… digit turns into a digit starting 011. The machine halts the next time the carry reaches it. We checked this directly: from w^5 01 0011^2 … it halts at step 248-250. - A (0RF, 0RA) and C: a glued 001011 halts at once. - F: five glued digits create a digit starting 01…. - A (0RF, 1RB), A (1RF, 0LD), D, E, G, H: no immediate halt for any glued digit. Some glued digits leave the language.
3. No digit in mxdys's language starts with 011, and every digit and w starts with 0. So, apart from the escapes, the rightward pass never meets 011 in phase.

In our runs every F entry had m ≥ MINM, so no glued escape and no m = 1 escape ever occurred. The exact halting condition for each line is therefore: a glued escape (or, in I and J, an m = 1 escape) with the listed next digit. Whether one ever happens is a question about the counter's exponents.

(c) Is there a digit-language invariant, so each F0 is checked once?

Yes, for everything except the glued cases. - The core rules never touch F, and they are shared by all 40 lines. They are exactly mxdys's table. - F0 and E1 only enter through the escape rule, and the 16 variants have only 10 escape rules (table above). So each class needs checking once, not each line. - Language closure in the runs. Every Inc boundary we parsed decomposed into mxdys's 25 digits on every line: all Incs up to 20,000, then every 64th, plus the Inc before and after every F entry. NONMX_LINE - Escape-rule closure. For positive exponents, each class's escape rule maps mxdys's language into itself, apart from the class D and I/J exceptions in (b).

What the invariant does not give is the arithmetic fact a proof needs: that exponent-0 merges at an escape (and the class D, I and J exceptions) never happen. That is the open question for stage 2.

(d) Nearest proved analogue, and why its proof fails

Proved neighbours were found by changing one field of (E1, F0); d01rule.json has the full list. We ran each method's representative for 15 s (runs/P_*.json):

The one useful lesson. The proved variants are proved because their escape is either frequent (hlin, TC decider) or it eventually locks the counter into a translated cycle that a 5^k-accelerated run can find (the three hand proofs). The holdouts' escapes are rare and feed the counter. For them the only known route is the second one: a far longer accelerated run.

A warning for direction 1: lines 64, 124 and 305 are not lockstep twins of Sk1like_TC_v1

Direction 1 plans to port mxdys's proofs to three lines: 64 and 124 (twins of TM1 and TM3) and 305 (twin of TM2).

At the digit level these are different variants. The holdouts are class H, (0RF, 1LB); his proof is for (1RF, 1RB). The core is the same, but the escape writes 0011001 where his writes 00001 01.

Why they ran in lockstep to 3e8. Usually the next carry turns both digits into 001101, so the two machines reconverge.

Where they part. For line 305 we traced the split: it comes when the escaped digit sits directly behind a 0011 with exponent 0. For 64 and 124 we only located it, after the 6th F entry. - his variant runs 0011^0 0000101 → 0011000101 → … → 0011101, which is a new escape; - ours runs 0011^0 0011001 → 0011011001 → …, which is not.

Measured with twin64.py (output in twin64.txt):

What this means for the port. Copying the TM1-TM3 modules will not close these lines. The 1.33M-step Inc chain runs into configurations where the holdout and the proved machine differ, so expect the port to fail coqc (direction 1's stop rule). These three lines belong to this family instead.