These three machines share a transition table, up to state renaming and reflection, but start it in different states. Each file proves nonhalting from the blank tape for its exact machine string.
| Machine | Start in the first table | Reflection |
|---|---|---|
1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF |
A | No |
1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF |
C | Yes |
1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA |
E | No |
The head bounces across five blocks of ones separated by short words. A twelve-trip rule moves these separators toward a collision. Two collision types alternate, giving a closed recurrence on a family Even(n,x):
Even(n,x) → Even(n + 12x + 808, x + 32)
n odd, x ≡ 4 (mod 8), x ≥ 52
The hypotheses are preserved, and every cycle takes positive time. Each blank start has its own finite opening into this family; merely renaming the first machine's blank-start theorem would not establish the other two results.
The proofs use Individual62, ES_v3 and the Rocq standard library. Symbolic execution proves the block rules, induction repeats them, and progress_nonhalt_simple closes the infinite recurrence.
The two alternate starts use Perm and, for the reflected machine, flip_halts. Each file concludes with Lemma nonhalt: ~halts tm c0.; Print Assumptions nonhalt is closed.
Full write-ups: https://github.com/DennisKoshta/busycoq/blob/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/chaotic-edge/README.md
AI assistance: Claude (Anthropic) assisted with the original formal proofs, proof sketches, scripts and checks. GPT-6 Astra (OpenAI) assisted with independent audit and submission preparation.
Validation: Freshly compiled with Coq 8.20.1 against unmodified busycoq BB6 at 9b1e92aead6c61d436495e6010e61eae32452879. A separate checker verifies the exact TM_from_str literal and blank configuration. Print Assumptions nonhalt is closed, and independent coqchk rechecking passes.
Downloads: write-ups ZIP · images ZIP.