Discord draft: kill announcement for 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF
Not posted. Paste the block below as one message. It is 1,741 characters before the link, under Discord's 2,000-character limit (a link of up to about 258 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF.v in this folder).
2. The duplicate-work question in our Discord drafts, Message 1, is marked not posted, and no reply is on file. Its group 3 is this machine and its twin. If it is still unsent, cut group 3 down to the twin, or drop it.
3. Discord was never searched for this string (observe.json discord_check points to that Message 1). Nothing on file says anyone has claimed it, but search #bb6 for the string before posting.
4. The twin 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB (row 833) is not formalized. The message says only that the same theorem should settle it (proof.md §6.1: a budget-2 edge lemma, then Eqv.v TM113.eqv).
5. No Checkpoint A or B notes from you were on file when this was packaged. If you add any, fold them into proof.md (the working copy and this folder's copy) first.
`1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF` (Counter Class 4, sheet row 832) never halts. Coq proof: <LINK>
The tape is a stack of runs of 1s and A runs it like a call stack: a push pays one 1 from the top run and makes the next run the new top frame, and a top run that is a lone 1 finishes and merges into the run below. An epoch starts at `0^inf <A 0 111 00 W`; its edge frame can make 3 children, and the machine halts only if an epoch needs a 4th. On `W = 1^a 00 1^b N` the epoch replays the machine's own history one level down on the marker tail N (lone 1s, even gaps) for a-1 inner epochs, each costing 2, or 3 when it absorbs a marker. The absorption law (inner epoch n costs 3 iff n is the sum of (gap-1) over the first j markers, for some j) is proved by induction on n + #markers, together with an invariant on where the unabsorbed markers sit. The top level has no markers, so every top epoch costs 2. In Coq, a big-step frame relation `Life` (one induction over 3 `es` rules lifts it to the TM) replaces the stack simulation, and marker words are lists of absorption indices, so the bookkeeping is shifted `Forall2` copies plus lia.
The twin `1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB` (row 833) is Eqv.v TM113's tm', and TM113's tm is this table started in B, so the same theorem should settle it too, but this file only proves the string above.
One file, top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c, imports only Individual62. Compiles in ~4 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.