Discord draft: kill announcement for 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB
Not posted. Paste the block below as one message. It is 1,825 characters before the link, under Discord's 2,000-character limit (a link of up to about 175 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB.v in this folder). If the URL is longer than 175 characters, drop the sentence "It is not a relabeling or mirror of 832 (all 1,440 checked)." (61 characters with its trailing space).
2. This message builds on the row-832 kill (#12, 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF), whose draft (discord.md in #12's package) is also unposted. Post #12 first. That draft's twin paragraph says the twin is not formalized ("this file only proves the string above"). Before posting it, cut that paragraph or change it to point at this message. You could also post the two as a pair, one right after the other.
3. Message 1 of our Discord drafts (not posted) asks about both machines as group 3. If it is still unsent, drop group 3.
4. Discord was never searched for this string. Nothing on file says anyone has claimed it (sheet row 833 has no notes or links). Search #bb6 for both strings before posting.
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.
`1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB` (Counter Class 4, sheet row 833) never halts. Coq proof: <LINK>
It's the twin of row 832 (`1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF`). Rename A..F to B,C,D,E,F,A and you get 832's table with one transition changed (A0 = 1RA instead of 1RB), started in B. It is not a relabeling or mirror of 832 (all 1,440 checked). That A0 (the twin's F0) is read only on the first step of the left-edge push, where the twin takes a 6-step detour (F0 F0 F1 B1 A1 A0 in its own names) to the configuration 832 reaches in 2 steps: same tape effect, 4 more steps. So 832's argument carries over verbatim: the run-length call stack, the epochs that replay the machine's history on a marker tail, and the absorption law (an inner epoch costs 3 iff it absorbs a marker, else 2). The only real change is the edge. The twin returns to `0^inf <F 0 11 00 W` instead of `0^inf <A 0 111 00 W`, so its edge frame can make only 2 children per epoch, not 3. The top level has no markers, so every top epoch costs exactly 2. That is zero slack, which is why it needs the exact cost law and not just "cost <= 3". In Coq, it's 832's file with the head state renamed, plus one new lemma that moves a cost-2 epoch onto the value-3 edge frame (`Life_shape` monotonicity), a 48-step init and the new top-level target. The rule lemmas, detour included, still close by plain `es`.
One file, top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c, imports only Individual62. It proves the holdout string directly (no Eqv.v TM113.eqv). 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.