W5-8b 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF
740 line 418 (byte for byte, once). Sheet: Results tab, class "Bouncer + Chaotic Edge", no status, notes, sources or "Done By"; level-0 tab: no status. Discord: only mxdys's UBRRBA_TODO list (data/discord/2026-08-24_mxdys_ubrrba_86.txt line 85, next to the parent on line 86), an acceleration to-do list, not a claim. busycoq: absent from the solved index (vendor 0940bb9), and the upstream tree at 9cf9e88 (+ our local PR commit 69c43b6) contains none of the 1,440 renaming/mirror variants of the table.
Same transition table as W5-8 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (740 line 214, the parent, KILLED_NONHALT),
mirrored, states renamed by sigma = A->B, B->C, C->A, D,E,F fixed (12/12 cells; the only map of 720 x 2). It starts
in A = sigma(C), so its run is the mirror of the parent's table run from 0^inf C> 0^inf. Mechanism, rules and the
double cycle: the parent's notes.md / proof.md.
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 58/58 PASS, seeds 1 and 2 default, and seed 1 --full (logs below).
- Relation (proof.md 1). Lemma M: Phi = mirror (position p -> -p) + state renaming sigma maps parent-table steps
to steps of this machine one for one, halts to halts (D0 is the only undefined cell of both; sigma(D) = D). Start
0^inf A> 0^inf = Phi(0^inf C> 0^inf). Left records become right records. The mirrored family:
Phi K(n,a,b,c,d) = 0^inf 1^3 0 1^2 0^2 1^2 0 1^d 0^6 1^4 0 1^2 0 1^c 0^6 1^b 0 1^2 0 1^a 0 1^n G^R F> 0^inf. Checked: lockstep with the parent's table from C at every step for 2e6 steps (Python), and mirror-equal tapes after 153,013,640 steps (C runner). - Opening (proof.md 2). Blank --(4,098,826 direct steps)--> Phi K(1953,34,68,45,18), the first K-shaped (right) record; the parent's table from C reaches K(1953,...) at the same step (first K-shaped left record). Then the parent's own 20-row chain (S^4 TO S^4 T6 S^6 T8 S^5 T6 S^12 T8 S^9 TO S^17 T8 S^13 T6 S^22 TE S^16 T6) with the same a,b,c,d in every row and n smaller by 6, ending at Even(12857,212) at step 153,013,640 (= the observe stage's figure). The parent's own opening: K(1959,34,68,45,18) at 4,097,897, Even(12863,212) at 153,126,993.
- Why the domains hold (proof.md 2.3). Every rule updates a,b,c,d independently of n and adds a constant to n, so the two runs keep equal a,b,c,d and a fixed n difference; the domains need only n odd. Same argument for the orbit: every even/odd run start of this machine to 1e10 has the a,b,c,d of a run start in the parent's run, n - 6 (check DC.orbit_same_abcd_as_parent_run_and_n_minus_6).
- Invariant (proof.md 3). Even(12857,212): 12857 odd, 212 = 4 mod 8, >= 52 = the whole domain of the double cycle; no adjusted invariant.
- Remark (proof.md 5). 740 line 636 (
1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA, start E of the table, not mirrored) reaches Even(13299,220) at step 163,638,058 (checked, REM). Not done here; it would be the same kind of delta (its own opening only). - check_proof.py (sections T, REL, K, OPEN, INV, DC, REM, PAR, HALT, DOC). It imports the parent's check_proof.py for the rule statements and K word, and its PAR section 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 runner scripts/krun.c (table + record side as arguments).
- Logs: work/check_proof_seed1.log, work/check_proof_seed2.log (default, ~95 s each),
work/check_proof_full_seed1.log (--full, 321 s, parent --full 196/196 inside); the parent's runs in
work/parent_check_proof_
_seed .log. After a last prose pass on proof.md (1.2, 6, header) DOC/INV/K were re-run: 11/11 (work/check_proof_doc_after_prose.log). - Teeth: n = 1955 instead of 1953 in the opening start -> 5 FAILs (OPEN, DOC); a wrong sigma (A->C, B->B, C->A) -> REL (4 checks) and DOC fail; one wrong step number in the proof.md table -> DOC fails.
- Independent simulator cross-check (outside check_proof.py): tools/sim.py's own engine (
sim.run) on this machine from blank gives Phi K(1953,34,68,45,18) at 4,098,826 and Phi Even(12857,212) at 153,013,640 (state F, word up to the head equal, nothing right of it). - Lint. proof.md before section 7 (sections 0-6): writeup_lint 0 errors, 0 warnings.
Next
- Checkpoint B (Dennis, non-blocking).
- Formalization (proof.md 6). Route 1 (conjugacy) is the short one: the parent's .v with its table renamed
tmP;flip_halts_iff(Flip.v) +perm_nonhalt(Permute.v) reduce~halts tm c0to~halts tmP (C;; tape0); new openingC;; tape0 -->* Kr 976 17 34 22 9(4,098,826 steps, cut at left records as the parent's six pieces), then the parent's 20 follows with N 3 smaller, ending atEv 6428 20;progress_nonhalt_simpleunchanged. - Posting: together with the parent (its submission/discord.md says the siblings are not formalized).
Kill
KILLED_NONHALT (2026-10-13), independently re-verified and packaged.
- Kill file 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF.v (407 lines, sha256 7bd5af92..26f0), route 1 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 : C;; tape0 -->* Kr 976 17 34 22 9 (4,098,826 steps, six cconfig_step pieces at left records), opening
= the parent's 20 follows with N - 3 to Ev 6428 20, nonhaltP by progress_nonhalt_simple, then
perm : Perm (flip tm) tmP phi + flip_halts + perm_halts (no flip_halts_iff, so no axiom).
- Audit: PASS (check_kill exit 0, 17/17; string byte-exact at 740 line 418; .v read end to end; all 12 cells of
Perm (flip tm) tmP phi checked by hand; 0 assumptions).
- Fresh check_kill on the unchanged file (same sha256): PASS 2026-10-13T13:00:14Z, compile 6.6 s native, coqchk
pass 44.4 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, section 6 on the finished .v, 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,377 chars without the link; post as a
reply after the parent's message, and first change the parent draft's "418/636 not formalized" sentence).
- Left: 740 line 636 (same table from E, not mirrored; reaches Even(13299,220) at 163,638,058) needs only its own
opening + Perm (no flip).
Re-dispatch as W5-8d (2026-10-13)
A workflow re-dispatched this machine as "W5-8d" for the delta-proof stage. It is already done (W5-8b,
KILLED_NONHALT, packaged), so nothing was redone and the label stays W5-8b (status.json alias_labels).
Re-checked: byte-exact once at 740 line 418; canon(this, A) == canon(parent, C), and C is the only start that
matches; the .v sha256 7bd5af92..26f0 is unchanged and equals the PASS run in rocq/check_kill_final.log;
check_proof logs 58/58 (seeds 1, 2 default; seed 1 --full); no sheet or Discord snapshot is newer than the kill.