Decision: K42 (40 lines, one Skelet-1 core) after stage 2
2026-10-14. Background: atlas.md in this folder; stage 2 is its last section. K42 has no machine folder, so this card lives here.
What we found
K42 is a cryptid family. All 40 lines run the same base-5 counter. They differ only in what happens when the counter meets the two-cell digit 01 (an "escape"), and the 16 variants come down to 10 escape rules.
Stage 2 ran every line far. We ported mxdys's own 5^k-step acceleration and checked it two ways: - it reproduces stage 1 exactly on all 40 lines; - it finds his two proved cycles with his exact periods.
Then every line ran to 10^139-10^153 counter increments in 40 seconds, and on to 10^169-10^194, on tapes of about 10^150 cells and more. mxdys's note on line 496 stops at a tape of about 10^64 cells.
Nothing settled. - No line halted. - No line fell into a repeating (translated) cycle. Every hand proof of a sibling on this core rests on such a cycle. The decider proofs (hlin) cover only variants that escape every ~100 increments, and these escape a few hundred times in 10^150. - 13,228 escapes in all, with no pattern in the digits around them.
Why it cannot be settled by running longer.
- A line can halt only if one escape ever finds an exponent of exactly 0 next to the 01.
- The numbers that can run down to 0 sit at the far end of the tape, in the oldest digits, and in a few small groups at the front. The far end changes about once per factor of 5 in run length, and a digit dies there only every few dozen to few hundred orders of magnitude of run length.
- Each death is one local event, decided by leftover residues of numbers with hundreds of digits.
- So the question is an endless series of pseudo-random trials. Our 40 continuations, about 1,100 orders of magnitude of run length in all, saw one of them.
- The one far-end mechanism we could isolate, a dying digit that turns the end into a glued escape, does not halt on any variant: 128 of 128 test runs recover. So a halt would need a rarer event still, and the evidence leans toward "never halts" without proving it.
Per the cryptid protocol the rules are written out (atlas, "The rules"), the family is flagged, and work has stopped. There are no kills, no predicted halts, and no proof route.
Options
| id | option | what happens | cost | odds (est.) |
|---|---|---|---|---|
| A | Park, flagged as a cryptid family (recommended) | The atlas (stages 1 and 2) is the record. K42 goes on the board and in the strategy file as "cryptid family, 40 lines, rules written". The ported simulator stays in reports/k42/ so any later step starts from it. | About 15 minutes (board line, strategy note) | 0 kills, and none expected from the alternatives either |
| B | Write the cryptid rules file in Rocq | Copy mxdys's Sk1like_TC_v2.v core (RInc, RIncs and their proofs) and replace his three escape rules with each class's rule. That gives 16 variant modules sharing 10 escape rules, plus a start lemma for each of the 40 lines and a short note. It proves the macro rules only, not "halts iff a glued escape" (the end of the tape leaves his digit language, so that needs more). Not a kill: check_kill does not apply. |
1-1.5 agent-days; a few coqc runs (the 2-coqc limit applies) | High that it compiles (about 0.8). List movement: 0. Credit: thin, since most of the file is mxdys's own core. |
| C | Fund a family-proof stage | Look for an invariant that rules out a glued escape at the far end, class by class. There is no candidate. The plain digit language is not even closed for mxdys's proved variants: 3 of 2,000 random tapes halt and 73-133 leave the language. A regular invariant would have to track residues. | 2 agent-days, then stop | Under 5% for even one class |
Recommendation: A
- B and C cannot produce kills. B only explains lines. C has no idea to fund: the cycle route is excluded to 10^139 increments, against 1.7×10^10 for the hardest proved sibling, and the plain regular-invariant route fails even on the proved variants.
- Nothing is lost by parking. The simulator is exact and validated. If someone (or Astra's new automaton search) finds an angle, B or C can start from this folder in minutes.
- If you want the cryptid on record anyway, B is the cheapest way to get it (about 1 day), but most of its content is mxdys's own file. A short note in #bb6 would carry the same information more cheaply; posting anything there is your call.
What I need from you: A, B or C.
Answer
Dennis, 2026-10-14: A (park, flagged as a cryptid family).