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 REACH_SHORT:
- 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 REACH_INCS Incs per line. Two routes remain:
- Port mxdys's 5^k-Inc acceleration (
RIncsinSk1like_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 howSk1like_TC_v2was 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. - 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)
| File | What it does |
|---|---|
k42sim.py |
Exact simulator. The tape is run-length encoded in 4-cell blocks, and the head works in a 2-cell-block window, so whole runs b^m are crossed in one step. Every TM step is counted, and it stops on exact step counts. |
validate.py, validate_1e9.jsonl |
Checks k42sim against tools/sim (C core) on all 40 member strings to 1e9 steps: final tape, state, head and every F-entry step agree on all 40 (ALL OK). |
digits.py |
Reads a configuration in mxdys's representation: 0^inf D> w^n d1 w^m1 d2 w^m2 ... 001 0^inf with w = 0001. The 25 digits are named by their bits (0011 = D0011, ...). |
mxinc.py |
A literal port of mxdys's RInc/Inc table from Sk1like_TC_v1.v. On his variant (E1 = 1RF, F0 = 1RB, start A), our reading of the TM agrees with his Inc on 63,943 consecutive increments, and reaches his x0 = (1, 0011^27 00001^8 001) at step 6,039. |
atlas_run.py, runs/ |
The long runs: one JSON per line (runs/L<line>.json) with every F entry, the digit configuration at the start of that increment and right after it, the digits seen, growth checkpoints and a translated-cycle detector. |
ruleprobe.py, d01rule.py, closure.py |
One-increment probes from hand-built digit configurations. They give the escape rule of every variant, held-out and proved (d01rule.json), and test it against every digit and exponent 0-6 (closure.json). |
analyze.py, fpattern.py, proved_summary.py, twin64.py |
The per-line data (atlas_data.json), the F-entry pattern search (fpattern.txt), the proved-neighbour runs, and the 64/124/305 twin check (twin64.txt). |
build_atlas.py, make_tables.py |
Generate this file from atlas_head.md, atlas_qa.md and the data. Edit those, not atlas.md. |
members.py, members.tsv, upstream_variants.py, upstream_variants.tsv |
The 40 lines (42 within 2 transitions), and every upstream machine on the core with the file naming it. |
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.