Discord draft: kill announcement for 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---
Not posted. Paste the block below as one message. It is 1,633 characters before the link, under Discord's 2,000-character limit.
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v in this folder).
2. The duplicate-work question to hipparcos (Message 2 of our Discord drafts) is marked not posted there, and no reply is on file. This kill is our string only, not hipparcos's Level 1 machine, but it is the same table. Consider posting in or linking hipparcos's Oct 2025 thread (https://discord.com/channels/960643023006490684/1432566675533992019) and @-mentioning him; the message names his machine without a ping. If Message 2 is still unsent, drop group 2 from it (group 1, pilot #3, still stands).
3. The twins (1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---, B-start, and the mirror 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---, C-start) are not formalized. The message says only that they reach the same invariant in simulation (proof.md §4, check 10).
4. No Checkpoint B notes from you were on file when this was packaged. If you add any, fold them into proof.md (working copy and this folder) first.
`1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---` (Skelet 1-like Class 2, sheet row 1284) never halts. Coq proof: <LINK>
The tape is a binary counter `0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b B> 0^inf` with digits `(10)^u 00 (01)^v` = 0 and `(10)^u (01)^v` = 1. Each macro step is one carry: every touched digit pays one `01`, a digit flipped to 1 gains a `10`, and a flipped digit with no `01` left merges into the next one. On overflow the digits are re-paired (the `(10)^u` halves become the `01` fuel of new 0-digits) and the counter restarts with one more digit. It could only get stuck if a carry reached a 0-digit with no `01` left. 20 window lemmas (`es`) compose into the carry, the carry with a merge, and the overflow, and a three-phase invariant (no merges / top digit about to merge / merged) of parities and 2^j bounds on the carries each digit still has to take is closed under all three. Architecture as SBCv6 TM21 (carries + re-pairing overflow), but one macro step per carry instead of a whole-cycle BigStep, since merges come at data-dependent times.
Same table as hipparcos's Level 1 machine `1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---` and its mirror, started in other states. Both reach the same invariant in simulation, but this file only proves the string above.
One file, top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c. Compiles in ~9 s, `Print Assumptions` closed, coqchk passes.
AI disclosure: the informal proof and the Coq formalization were produced with Claude Code (AI-assisted) under my direction, and checked by compiling against unmodified busycoq, with Print Assumptions and coqchk.