W5-8c 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA
740 line 636 (byte for byte, once). Sheet: Results tab, class "Bouncer + Chaotic Edge", no status, notes, sources or "Done By"; level-0 tab: status "-"; classifications tab: only in the "Bouncer + Chaotic Edge" column. Discord: only mxdys's UBRRBA_TODO list (data/discord/2026-08-24_mxdys_ubrrba_86.txt line 87, next to W5-8b on 85 and the parent on 86), an acceleration to-do list, not a claim. busycoq: absent from the solved index (vendor 0940bb9), and the upstream tree at 9cf9e88 contains none of the 1,440 renaming/mirror variants of the table. Singleton group in 2026-10-07_eqv_1590.txt (line 1879).
Same transition table as W5-8 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (740 line 214, the parent, KILLED_NONHALT),
not mirrored, states renamed by sigma = A->E, B->C, C->D, D->F, E->A, F->B (12/12 cells; the only map of 720 x 2).
It starts in A = sigma(E), so its run is the parent's table run from 0^inf E> 0^inf, renamed, on the same tape.
canon(this, A) = canon(parent, E) = 1LB0LC_0LD0RB_1RE1LA_0LC1LC_1LD1RF_---1RA (also with the scratchpad starts.py).
Mechanism, rules and the double cycle: the parent's notes.md / proof.md. The mirrored sibling W5-8b (line 418,
start C) is KILLED_NONHALT too; with this machine all three list entries of the table are covered.
Delta proof stage (2026-10-13)
Task: delta proof.md (relation, the exact opening run from blank into the parent's invariant, and that it holds there), validated in check_proof.py.
Result: proof.md complete and validated; status CHECKPOINT_B (non-blocking). check_proof.py 83/83 PASS, seeds 1 and 2 default, and seed 1 --full (373 s; orbit to 1e10: 30 even/odd run starts, 1,606 K-shaped left records, all predicted). DOC/OPEN/INV/PLAN re-run 39/39 after the last prose pass (work/check_proof_doc_after_prose.log).
- Relation (proof.md 1). Lemma R: renaming by sigma maps parent-table steps to steps of this machine one for one, halts to halts (D0 / F0 = sigma(D)0 the only undefined cells). No mirror, so left records stay left records and the family K is the same tape with head state sigma(F) = B. Checked: lockstep with the parent's table from E at every step for 2e6 steps (Python; 1e7 --full), and equal tapes after 163,638,058 steps (C runner).
- Opening (proof.md 2). Blank --(6,950,830 direct steps)--> K(2583,70,76,43,18), the first K-shaped left record
(in any state). Then 18 macro steps by the parent's rules, with its own chain
S^8 T6 S^7 TE S^6 T6 S^13 T8 S^10 TO S^18 T8 S^14 T6 S^23 TE S^17 T6(unlike W5-8b, not the parent's chain: a,b,c,d start elsewhere), ending at Even(13299,220) at step 163,638,058 (= the parent's §7.3 / W5-8b REM figure). All 125 transitions between consecutive K-shaped left records were explained by S/TE/TO/T6/T8 (scripts/chainfit.py); no new rule was needed. - Domains (proof.md 2.3). Row-by-row table: smallest a in an S block is 10 (row 9: S^10 from a = 82); all collision rows well inside (TE b >= 140, d >= 46; TO b = 126, c = 117, d = 58; T6 b >= 106, c >= 43, d >= 42; T8 b >= 156, d >= 70). n odd: starts at 2583, every rule adds an even constant.
- Invariant (proof.md 3). Even(13299,220): 13299 odd, 220 = 4 mod 8, >= 52 = the whole domain of the double cycle; no adjusted invariant. Orbit x = 220 + 32j (the parent's is 212 + 32j).
- Formal delta (proof.md 6). Start
Kr 1291 35 38 21 9, endEv 6649 21, the 18 follows with exact arguments (scripts/follow_args.py; check PLAN compares them with the lemma statements read from the parent's kill file). Bridge:Perm tm tmP phi(phi = sigma^-1, phi A = E) +perm_halts; no flip. - check_proof.py (sections T, REL, OPEN, INV, DC, PLAN, REM, PAR, HALT, DOC). Imports the parent's check_proof.py for the rule statements and K word; PAR runs the parent's check_proof.py in the same mode and seed (196/196) and requires its MR (symbolic proofs of S, TE, TO, T6, T8), DC and HALT sections. Own C tools: scripts/krun.c (W5-8b's batch runner, table + record side as arguments) and scripts/kscan.c (K-shaped left records by run-length parse). The strongest checks: the K-shaped left records of both runs up to 163,638,058 are exactly the 126 predicted points (start, every single application, end), and every K-shaped left record of this machine from there to 2e9 (1e10 --full) is the next point predicted by S, TE, TO (554 points to 2e9).
- Logs: work/check_proof_seed1.log, work/check_proof_seed2.log (default, 105 s each),
work/check_proof_full_seed1.log (--full, 373 s, parent --full 196/196 inside); the parent's runs in work/parent_check_proof_
_seed .log. - Teeth (scratchpad w58c_teeth.py, module-level mutations): n = 2585 in the opening start -> 9 FAILs (OPEN, PLAN, DOC); a wrong sigma (A->D, C->E) -> REL (4 checks) + DOC fail; S^7 instead of S^8 in row 1 -> 6 OPEN checks fail; one wrong step number in proof.md (46,448,503) -> DOC fails; one wrong follow argument -> PLAN fails.
- Independent cross-checks. The C K-scanner agrees with a regex scan (scripts/lrec.c + scripts/kscan_regex.py, observe-stage tool) on all 126 records to 163,638,058, for the parent's table from E and for this machine from A; tools/sim.py's own event engine finds the first K-shaped left record at 6,950,830 (check OPEN).
- Lint. proof.md sections 0-6: writeup_lint 0 errors, 0 warnings.
Next
- Checkpoint B (Dennis, non-blocking).
- Formalization (proof.md 6): copy W5-8b's kill file route (rocq/assemble.py there builds it from the parent's
file) minus the flip:
tm= this string,tmP= parent; newinit : E;; tape0 -->* Kr 1291 35 38 21 9(6,950,830 steps; the parent used six cconfig_step pieces for 4.1M because one piece made coqchk run out of memory under the 8 GB cap, so plan about ten pieces here, cut at left records);opening= the 18 follows of proof.md 6 toEv 6649 21;nonhaltP : ~halts tmP (E;; tape0)by progress_nonhalt_simple from (6649, 21);perm : Perm tm tmP phiwith phi = A->E, B->F, C->B, D->C, E->A, F->D;nonhaltbyperm_halts. - Posting: together with W5-8 and W5-8b (their discord drafts still say line 636 is open).
Files
- proof.md, check_proof.py, status.json.
- scripts/: krun.c (copied from W5-8b), kscan.c (K-shaped left records), lrec.c + kscan_regex.py + rows.py + chainfit.py + follow_args.py (observe/derivation helpers).
- work/: krun, kscan, lrec (binaries); kscan_parent_E.txt / kscan_this_A.txt (regex scans) and kscan_c_parent_E.txt (C scan) to 163,638,058; check_proof logs.
Kill
KILLED_NONHALT (2026-10-13), independently re-verified and packaged.
- Kill file 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA.v (458 lines, sha256 8c597d87..0584), route of proof.md 6:
the parent's kill file with its table as tmP (es' rules S/TE/TO/T6/T8, S_iter, DC unchanged), new
init : E;; tape0 -->* Kr 1291 35 38 21 9 (6,950,830 steps, ten cconfig_step pieces at left records), opening
= its own 18 follows to Ev 6649 21, nonhaltP by progress_nonhalt_simple, then perm : Perm tm tmP phi +
perm_halts (no flip). Built by rocq/assemble.py; details in rocq/log.md.
- Audit: PASS (check_kill exit 0, 17/17; string byte-exact at 740 line 636; .v read end to end; all 12 cells of
Perm tm tmP phi checked by hand, F0 -> D0, A -> E; 0 assumptions). Minor style note, not acted on: the header's
template line reads "Adapted from the proof for tmP, which follows verify/TranslatedBellv5.v, Module TM1" (same
wording as W5-8b's shipped file; changing it would change the audited sha256).
- Fresh check_kill on the unchanged file (same sha256): PASS 2026-10-13T13:33:44Z, compile 7.84 s native, coqchk
pass 64.86 s, 0 assumptions; only warning the second TM_from_str literal (tmP). Log: rocq/check_kill_final.log.
- Package submission/: the .v, public proof.md (rewritten from the working one: header with template / .v map,
summary, notation, sections 1-5 unchanged in substance, section 6 on the finished .v with the ten-piece table,
section 7 numerical checks; writeup_lint 0 errors, 0 warnings), parent-proof.md (the parent's public write-up,
for the P§n references), check_kill.txt (fresh run, paths as placeholders), README.md, discord.md (not posted;
1,292 chars without the link; post as a reply after the 214 and 418 messages, and first change those drafts'
"636 not formalized" sentences).
- With W5-8 (214) and W5-8b (418) all three 740 entries of this table are killed.
Re-dispatch as W5-8e (2026-10-13)
A workflow re-dispatched this machine as "W5-8e" for the delta-proof stage. It is already done (W5-8c,
KILLED_NONHALT, packaged), so nothing was redone and the label stays W5-8c (status.json alias_labels).
Re-checked: byte-exact once at 740 line 636 (no CR); canon(this, A) == canon(parent, E), and E is the only start
that matches; the .v sha256 8c597d87..0584 is unchanged, equals the submission copy and the PASS run in
rocq/check_kill_final.log; check_proof logs 83/83 (seeds 1, 2 default; seed 1 --full); the upstream 9cf9e88 verify
tree contains neither this string nor the parent's or W5-8b's; no sheet or Discord snapshot is newer than the kill.