K42 F-entry atlas (stages 1 and 2)

Stage 2 result (last section): with mxdys's 5^k acceleration, exact on all 40 lines, every line ran to 10^169-10^194 Incs with no halt and no translated cycle. Verdict: a cryptid family. The rules are written out there, and the decision for Dennis is in decision.md.

2026-10-14. Strategy direction 2 (reports/strategy/directions.md, section 2 and the Critic). Everything here is in reports/k42/. All machines are written in core naming: 1RB0RC_1LC0RD_0LD0LC_1RE0LA_0RA<E1>_<F0>---, started on a blank tape in the member's start state. A mirrored member behaves identically, so it gets the same treatment.

In plain words

All 40 lines run one and the same counter: the Skelet-1-like counter that mxdys wrote down in Sk1like_TC_v1.v.

The counter never uses state F. F is entered at exactly one kind of moment: when the counter's carry runs into the two-cell digit 01. What the machine does next is the only thing that differs between the 40 lines.

That difference is a one-line rule per line. It says at which point of the counter's digit cycle the 01 is put back in. The 16 (E1, F0) variants give only 10 different rules, called escape classes A-J below.

Nothing settles within our reach. We ran every line for 2.4-4.6 million counter increments (5.4e12 to 4.0e13 steps, tapes of 7.2e6 to 1.4e7 cells): - no line halted; - no line repeated its configuration the way mxdys's proved siblings do (a "translated cycle"); - every F entry was an escape with a positive exponent after the 01, the harmless kind.

Verdict: all 40 are "unclear". They are Skelet-1-type counters, very likely non-halting, but with no route yet. There is one exact way to halt, and we can state it per class (question (b)). Six lines (classes I and J) halt at once if it ever happens; six more (class B) halt one carry later.

Answers in brief: - (a) There is only a partial recurrence. Escapes at the front of the tape come at n = 100·25^k − 11 or 400·25^k − 11, a base-5 pattern; everything else is irregular. - (b) E reads 11 only after a "glued" escape. The exact digit per class is in (b). - (c) Yes. The core preserves mxdys's 25-digit language, and each of the 10 escape classes needs checking once. The 40 lines form 21 distinct histories. - (d) Each class's nearest proof fails for a stated reason, see (d).

A finding for direction 1. Lines 64, 124 and 305 are not lockstep twins of Sk1like_TC_v1. Their digit histories leave mxdys's after the 6th, 6th and 3rd escape, so the planned ports should be expected to fail (last section before the tables).

Recommendation for stage 2. Running longer at the Inc level is pointless; it is already 2.4-4.6 million Incs per line. Two routes remain:

1. Port mxdys's 5^k-Inc acceleration (RIncs in Sk1like_TC_v2.v, which moves n to n + dn + 5^k in one step) to Python. Then run one line per digit history (21 distinct histories once twins are grouped; see the tables) until a translated cycle appears. This is how Sk1like_TC_v2 was proved, after 1.7e10 accelerated macro-steps. It failed for line 496 at a tape of about 10^64, but nobody has reported runs for the other 9 classes.
2. Find an invariant on the exponents that rules out a glued escape (exponent 0 right after the 01; see (b)). This is a question about the counter's arithmetic, so it is cryptid-like. Per the protocol, the rules are written down here and the family is flagged.

Route 1 is cheap (Python, a day) and can be stopped at any point. Route 2 is a research problem.

What was built (all Python, stdlib only)

How the counter works

A configuration at the start of an increment ("Inc") is

0^inf  D>  w^n  d1 w^m1  d2 w^m2  ...  dk w^mk  001 0^inf        (w = 0001)

One Inc is a pass to the right and back: - D sweeps right over w^n; - the carry is handed from digit to digit (mxdys's RInc, which recurses through 00111); - the head returns to the left end.

Each digit runs through a five-phase cycle:

0011 -> 0011001 -> 001101 -> 00111 -> (carry into the next digit) -> 00101 -> 0011

Its exponent drops by two per cycle and grows by whatever the carry hands back. Meanwhile w^n at the front gains one w per Inc, until a carry packs it into a new 0011 digit and n restarts at 1. When an exponent reaches 0, mxdys's rules merge neighbouring digits, and some of those merges produce the digit 01.

State F is used nowhere in the core rules. On mxdys's own variant, only three of his rules run through F: 01^m, 00101^0 00101^m and 0011101^m. The last two reduce to the first, because the counter builds a 01 at the front of the carry during the Inc. So F is entered exactly when the rightward carry pass, in phase D, meets a 01: D reads the 0 and E reads the 1.

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)

This holds for 97 of the 165 depth-0 00101^0 00101 escapes in all 40 runs. The others, and every escape of another kind or at greater depth, fit no such formula (fpattern.py).

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 ≥ 3 (327 F entries over the 40 lines), 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. Digits outside the 25 that appeared: 000001, only in class D (see (b)). - 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.

Per-member tables

Each line ran for 45 or 80 s of Python: 2.4M-4.6M Incs, 5.4e12-4.0e13 steps, tapes of 7.2e6-1.4e7 cells. Verdicts: - unclear (counter; no TC in reach): no halt, no repeat of the tape front (translated-cycle detector: the 12 runs nearest the head, compared at every Inc boundary with content-defined 1/16 sampling; it finds mxdys's cycle on his proved variant at Inc 1.35M), and no glued escape. - Lines that halted: none. - Lines with a front repeat: none.

How to read the columns: - F entries gives the Inc numbers of the F entries (one Inc is one counter increment). - escape contexts says which of the three contexts fired and how often. - twin names another line whose configuration at its F entries is identical apart from the exponent of the deepest digit, with the number of shared F entries and the Inc offset. Most twins differ only in the start state (offset 0 or 13 Incs) or in F0 within one escape class. The pair 100/578 spans classes C and E, whose escapes end in the same digits one carry apart. Grouping the twins gives 21 distinct histories: {44 494}, {64 124}, {67 263}, {86}, {92}, {100 578}, {121}, {129 411}, {208 703}, {260 404}, {266 321 664 688}, {285 421}, {305}, {306 361 587 673}, {335 491 496}, {405}, {407 571}, {413 420}, {435}, {709 718}, {713}. One proof per group would do, as long as no carry reaches the deepest digit (the twins can differ there).

Escape class A: (E1, F0) = (0RF, 0RA), (0RF, 1RB), (1RF, 0LD)

Escape rule (one Inc, 01 at the front of the carry): w^n 01 w^m r → w^(n+1) 00101 w^(m-1) r.

Halting trigger (closure.py): for (0RF, 0RA), a glued escape (m = 0) followed by 001011 halts at once; (0RF, 1RB) and (1RF, 0LD) have no glued context that halts at once.

Escape class B: (E1, F0) = (0RF, 0LA), (0RF, 1RC), (1RF, 1LB)

Escape rule (one Inc, 01 at the front of the carry): w^n 01 w^m r → w^1 0011 w^n 001 w^(m-1) r.

Halting trigger (closure.py): a glued escape followed by any 0011… digit (or 001011) creates a digit starting 011, which halts the next time the carry reaches it.

Escape class C: (E1, F0) = (1RF, 0LA), (1RF, 1RC)

Escape rule (one Inc, 01 at the front of the carry): w^n 01 w^m r → w^(n+1) 00111 w^(m-1) r.

Halting trigger (closure.py): a glued escape followed by 001011 halts at once.

Escape class D: (E1, F0) = (1RF, 0RC), (1RF, 1RE)

Escape rule (one Inc, 01 at the front of the carry): w^n 01 w^m r → w^(n+1) 001101 w^(m-1) + the carry runs on into r.

Halting trigger (closure.py): no glued context halts at once. An escape followed by 001, 0010101 or 001011 (any m) creates 000001. This happened on 4 of the 6 lines (306, 361, 587, 673), at their first escape, with no harm.

Escape class E: (E1, F0) = (1RF, 0RE)

Escape rule (one Inc, 01 at the front of the carry): w^n 01 w^m r → w^(n+1) 001111 w^(m-1) + the carry runs on into r.

Halting trigger (closure.py): no glued context halts at once, and all of them stay in the language.

Escape class F: (E1, F0) = (0RF, 0LC)

Escape rule (one Inc, 01 at the front of the carry): w^n 01 w^m r → w^(n+1) 00001 w^(m-1) r.

Halting trigger (closure.py): no glued context halts at once; five of them create a digit starting 01 (not traced further).

Escape class G: (E1, F0) = (0RF, 0LB)

Escape rule (one Inc, 01 at the front of the carry): w^n 01 w^m r → w^1 0011 w^(n-1) 001 w^m r.

Halting trigger (closure.py): no glued context halts at once, and all of them stay in the language.

Escape class H: (E1, F0) = (0RF, 1LB)

Escape rule (one Inc, 01 at the front of the carry): w^n 01 w^m r → w^1 0011 w^(n-1) 0011001 w^(m-1) r.

Halting trigger (closure.py): no glued context halts at once; some leave the language.

Escape class I: (E1, F0) = (0RF, 0RD)

Escape rule (one Inc, 01 at the front of the carry): w^n 01 w^m r → w^(n+1) 00111 w^0 0011 w^(m-2) r (m ≥ 2).

Halting trigger (closure.py): a glued escape followed by any 0011… digit halts at once; so does m = 1 followed by 001011.

Escape class J: (E1, F0) = (0RF, 1RD)

Escape rule (one Inc, 01 at the front of the carry): w^n 01 w^m r → w^(n+1) 00001 w^0 0011 w^(m-2) r (m ≥ 2).

Halting trigger (closure.py): a glued escape followed by any 0011… digit halts at once; so does m = 1 followed by 001011.

Reproduce

All Python 3, stdlib only, from reports/k42/:

python3 -B members.py 1 > members.tsv                 # the 40 lines
python3 -B validate.py 1e9                            # k42sim vs tools/sim on all 40 (4 s + 0.2 s each)
python3 -B d01rule.py; python3 -B closure.py           # escape rules, closure (about 1 min)
runs/run_all.sh 80; runs/stage2_batch.sh               # long runs (2 processes, nice 10, ulimit -v 6e6)
python3 -B analyze.py; python3 -B fpattern.py; python3 -B build_atlas.py

runs/L<line>.json has, for each F entry: - the exact step and Inc number; - the digit configuration at the start of that Inc and right after it; - whether mxdys's own table would have made the same move (never, for a holdout escape: that is the variant difference); - the tape around the head in gap form.

Stage 2 (2026-10-14): the 5^k acceleration, and the verdict

In plain words

We ported mxdys's 5^k-Inc acceleration (RIncs from Sk1like_TC_v2.v) to Python and made it exact for all 16 variants: anything the shared core table does not cover is handed to the real machine.

It is exact and it finds his cycles. - From each line's first F entry it lands on stage 1's final configuration digit for digit, 2.4-4.6 million Incs later, on all 40 lines, with all 327 F entries in between. - On his two proved variants it finds his translated cycles with his exact periods: 669,180 Incs (Sk1like_TC_v1) and 518 Incs after 1.73e10 Incs (Sk1like_TC_v2).

Every line ran to 10^139-10^153 Incs in 40 s, then on to 10^169-10^194 Incs. mxdys's note on line 496 stops at a tape of about 10^64 cells. Nothing settled: - no line halted; - no line entered a translated cycle; - 261-443 escapes (F entries) per line, 13,228 in all.

The tape is a base-5 odometer, and that makes simulation hopeless. - The number of digits is log5(Incs), within 2. - The front holds huge numbers. The only exponents small enough to run down to 0 sit at the far end of the tape (the oldest digits) and in a few recurring "front gadgets" (classes B and G). - Halting needs an exponent of exactly 0 at an escape, so only those places matter. - The far end changes once per factor of 5 in Incs, and a digit dies there far more rarely still. Across the 40 continuations, which cover about 1,100 orders of magnitude of Incs in all, it happened once.

Verdict: (ii), a cryptid family. Whether a line halts depends on the outcome of an endless series of rare events at the tape's end. Each outcome is set by the residues of numbers inherited from the front, which have no pattern we can find.

Per the cryptid protocol: the exact rules are written below, the family is flagged, and the work stops here. There are no kills and no predicted halts. No family-proof route was found: the translated-cycle route is ruled out far beyond any reach that has produced a proof, and the digit language is not a regular invariant even for the proved variants.

What was built (stage 2; Python, stdlib only)

Validation and calibration

Exact reproduction (accel.py validate, all 40 lines). - Start: the configuration at the line's first F entry (stage 1, Inc 127-140). - Run: exactly as many Incs as stage 1 ran, in 1,048-1,844 accelerated macro steps. - Result: the same tape as stage 1's last configuration on all 40 lines, and the same F entries (327 in all). - Line 121 matches only once stage 1's Inc count is corrected (erratum below).

Core table against the machine. On the first 3,000 Incs after each line's first F entry, every Inc the F-free core table covers agrees with the machine: 119,885 of 119,885.

The second F context reduces to the first. One Inc from w^a 00101 00101 w^m r and from w^(a+2) 01 w^m r gives the same tape: - on all 16 variants; - at the front and behind a 00111 digit; - for random tails, m = 1-4 and a = 1-5; - 6,400 of 6,400 cases.

The third context, 0011101 w^m, is literally the tape 00111 01 w^m.

Calibration on mxdys's proved variants (calib.py, 30 s each, from his x0 = (1, 0011^27 00001^8 001)):

So the detector finds both of mxdys's cycles, with his exact periods.

Errata for stage 1. - Inc numbers. Stage 1 skipped Inc boundaries whose tape did not parse into mxdys's digits, so its Inc numbers are low: - by 2 or 11 on 26 lines, all of them before the first F entry, so differences and twin offsets are unaffected; - by 52 on line 121, 50 of them after its first F entry. - mxdys's cycle length. His Inc_Sn 669179 runs 669,180 Incs, so the cycle is 669,180 Incs, not 669,179. Stage 1's own measurement, 1,338,360 Incs = 2 × 669,180, was right.

The rules (cryptid protocol: written out)

1. Configuration (at the start of an Inc, core naming):

0^inf  D>  w^n  d1 w^m1  d2 w^m2  ...  dk w^mk  001 0^inf        (w = 0001, n >= 1)

Here d1..dk are mxdys's 25 digits (digits.MX). Rarely a digit falls outside them, such as class D's 000001 or a rewritten end of tape (below). Such cases are run on the machine itself.

2. Core (shared by all 16 variants; F is never entered). This is mxdys's RInc/Inc table of Sk1like_TC_v1.v and Sk1like_TC_v2.v with the rules that run through F removed (our port: mxinc.py; the F-free cut: accel.core_rinc). The digit cycle is

0011 -> 0011001 -> 001101 -> 00111 -> (carry into the next digit) -> 00101 -> 0011

Each digit's exponent loses 2 per cycle and gains what the next digit hands back. Exponent-0 merges follow his table.

3. Acceleration (all variants). Suppose d1..dk are all cycle digits (00101 0011 0011001 001101 00111) with m_j >= 2·5^(k-j). Then 5^k Incs take

n -> n + 5^(k-1) + 5^k
m_j -> m_j - 2·5^(k-j) + 5^(k-j-1)     (j < k)
m_k -> m_k - 2 + dn

Meanwhile the rest of the tape receives exactly one carry, which must return Tp0 with dn. This is RIncs_spec in Sk1like_TC_v2.v. Its proof only uses passes over the five cycle digits, which never reach state E or F, so it holds for every (E1, F0).

4. Escape: the only rule that depends on the variant. F is entered exactly when the carry meets a 01. Each class has one rule: what one Inc does to w^n 01 w^m r for m >= 1 (m >= 2 in classes I and J). The ten rules are in "The ten escape rules" above. The other two F contexts reduce to this one: - 00101^0 00101^m acts as 01^m with 2 more w in front (checked above); - 0011101^m is 00111^0 01^m.

5. Halting. F reads a 1 only after a glued escape: m = 0, or m = 1 in classes I and J. Which next digits make it halt, at once or one carry later, is listed per class in (b). So a line can halt only if some escape is ever glued.

Results per line (40 s each)

"Smallest m" is the smallest exponent after the 01 at any F entry. The last column is the far end of the tape at the end of the run (the terminal 001^0 last).

What the table shows: - No halts, and no translated cycle. Exact repeats of n and the first 4 digits did occur on lines 64, 124 (1 each), 709, 718 (10 each) and the 6 class-B lines 67, 263, 266, 321, 664, 688 (50 each). Each is a short "front gadget" re-forming after the front resets: for example n=1 | 0011^3 00001^91 0011^1630 001101^0 … on line 67, at Incs 3.9e8, 6.2e9 and 2.1e24. The intervals grow, so this is not a cycle. The digits behind the gadget differ each time. - Escapes are mostly at the front (70%), with m growing with the scale. - The small m values come from two places: - recurring front gadgets in class B: m = 934 (lines 67, 263) and 1632 (266, 321, 664, 688). These come back with the same value again and again; line 67 has m = 1632 at Incs 1e8.6, 1e9.8, 1e24.3, 1e38.5, 1e68.4 and 1e92.0. Class G's smallest value, 47,884 (lines 709, 718), is a single escape deeper in the tape at Inc 1e19; - the tape's far end: m = 6 on lines 44 and 494 at Inc 1e48, an escape 01^6 001 against the terminal.

Where a halt could still come from: the far end of the tape

New digits are made at the front, so the oldest digits sit at the far end. Each far-end digit changes about once each time a carry runs the whole tape, and a whole-tape carry comes once per factor of 5 in Incs. Here is line 285 (class J) traced from Inc 1e6 to 1e188 (endtrace.py, cont.py; the last 4 digits, terminal last):

The pattern holds on every line we traced: - the last digit's exponent barely moves: it stays within 1-3 of a fixed value (0-1 on line 285, 3-4 on line 44 after its death at Inc 1e48, 447,605-447,606 on line 435); - the next digits lose a steady amount per digit added to the tape (about 37 and 187 on line 285), until one dies; - then an older digit, with a much larger exponent, moves up. Line 285: the 1,392 digit runs out at Inc 1e166 and the 111,792 digit moves up. Line 44: the 35 digit runs out at Inc 1e48 and the 50,750 digit moves up.

Each death is a single local event. Its outcome depends on the phases of the dying digit's neighbours at that moment, that is, on residues of numbers inherited from the front long ago.

• Counted. The 40 continuations (from about 1e148 to 1e169-1e194, 1,097 orders of magnitude in all) show 1 death at the far end, on line 285 (enddeaths.py). The line-44 trace from Inc 1e6 shows 1 more, at Inc 1e48. Neither halted.
• How a death makes an escape. On line 44 at Inc 1e47.7 the tape end read 00101^0 001101^6 001. mxdys's rule 00101^0 001101 -> 01 turned it into the escape 01^6 001, where m = 6 is the last digit's exponent. On line 285 the last digit's exponent is 0 or 1, so a glued escape at the end is not ruled out by size.
• Such glued deaths are survivable. We started every variant from w^5 0011^a 00101^0 001101^m 001 with a = 40, 41 and m = 0-3, and ran 10^7 Incs (endglue.py). None of the 128 runs halted; every one rebuilt an ordinary end of tape. So a halt would need something rarer: a death further from the end, or a front gadget drifting to 0.
• Escapes next to the terminal never halt at once. We tested 01^m 001, with and without a 00111^0 in front, m = 0-2, on all 16 variants. Several rewrite the end of the tape: class D makes 000001; class F with m = 0 deletes the terminal, leaving only w^7. The endglue.py runs pass through exactly these escapes (m = 0-3) and recover.

Why simulation cannot settle it. The next digits at the far end lose only tens to hundreds per digit added to the tape, so a death there is separated from the next by tens to hundreds of orders of magnitude of Incs. Our runs saw 0 or 1 per line. A halt needs one specific outcome, out of an unbounded series of such events, whose inputs are residues of numbers with hundreds of digits.

The digit map at the escapes

At each escape the counter hands the escape rule two values: the exponent m and the next digit (digitmap.py). - Next digit. Over all 13,228 escapes, all five phases occur: 0011 2,114, 0011001 1,328, 001101 5,651, 00111 2,789, 00101 1,344, other 2. - No periodic tail. On no line is the second half of the next-digit sequence periodic, nor that of m mod 5. Line 44's first 90 escapes, coded a-e for the phases in the order above:

bbcddaedddccaadaacaacddbbdddeeecdaabaacccccdaacdacbbcdddddacddaacdedabbccbbccbbacecddaacee

• The front escapes are regular; the rest are not.
• The front escapes follow the base-5 times n = 100·25^k − 11 and 400·25^k − 11 of stage 1 (a). For example, one of line 44's front escapes has n = 100·25^42 − 11 (about 5.2e60).
• The exponents they carry, and every escape deeper in the tape, follow no formula stage 1 could find. Here their next digits and residues show no period either.

Is the digit language a regular invariant? No

If one Inc mapped every tape of mxdys's language into the language without halting, the language itself would prove nonhalting. It does not, for any variant. We ran one Inc from 2,000 random tapes of the language per variant (exponents 0-3, closure2.py):

The proved variants fail too, so the reachable tapes are a thin subset of the language. A regular invariant would have to track which phases can meet at the far end, which is the arithmetic above. No upstream decider closes any of the 16 holdout variants, and the critic's hlin run at the proving configuration was 0 of 8 (stage 1 (d)).

Verdict

• (i) Family-proof route: none found. The only proof shape that has closed this core is a translated cycle found by a long accelerated run. It is excluded here to 10^139-10^153 Incs on every line, and to 10^169-10^194 Incs on all 40 in the continuations. That is far beyond the 1.7e10 Incs that Sk1like_TC_v2 needed.
• (ii) Cryptid: yes. The rules are in the section above. The halting question is "does one of infinitely many far-end deaths (or a drifting front gadget) ever give m = 0 with the class's next digit?", and the inputs to each death are residues of inherited huge numbers. Flagged; stopped.
• (iii) Predicted halts: none. No halt to 10^169-10^194 Incs, and no small-m trend that points to one.

Reproduce (stage 2)

From reports/k42/; each step is 2 processes, nice 10, ulimit -v 6e6:

python3 -B accel.py validate 44 64 ...        # exact reproduction of stage 1 (seconds per line)
python3 -B calib.py 30                         # mxdys's two cycles
python3 -B rules2.py 200 7; python3 -B closure2.py 2000 1; python3 -B endglue.py
runs2/run_all.sh 40                            # 40 s per line -> runs2/A<line>.json
runs2/cont_all.sh 30; python3 -B cont.py 285 60; python3 -B cont.py 713 60
python3 -B analyze2.py; python3 -B digitmap.py 44; python3 -B enddeaths.py; python3 -B build_atlas.py