W4-3c 1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD

740 line 588 (778 line 624). Sheet: Results tab, class "Skelet 1-like Class 2", no notes or claims. busycoq verify/ has no completed proof (byte-exact, renamed or mirrored; it appears only as an equivalence endpoint).

Same transition table as W4-3 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA--- (740 line 341, the parent), states renamed by phi = A->F, B->A, C->B, D->C, E->D, F->E after mirroring L <-> R (12/12 entries; the only map). It starts in A = the parent's F, so it runs the parent's table from 0^inf F> 0^inf (mirrored). Mechanism, invariant and informal proof: the parent's notes.md / proof.md (its section 9 already covered this start in simulation).

Class 2 close-out, stage 2 (2026-10-12)

Track: the W4-3 table (740 lines 341, 512, 588), funded sync_stage. When this stage started the parent (341) was already killed (check_kill PASS; parent notes.md ## Kill), so the stage formalized the two other starts of the table.

Result: KILLED_NONHALT (check_kill PASS). Lemma nonhalt: ~halts tm c0. in 1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD.v (2,621 lines, sha256 48b42caf..d1d3, Individual62 + stdlib only). check_kill: PASS, compile 72.31 s (run alongside other sessions' Coq jobs), Print Assumptions closed (0 assumptions), coqchk timeout (600 s cap; policy A warning, as for the parent). Warnings: the second TM_from_str literal (tmP), plus the standard native-compiler and coqchk-timeout notes.

• File = the parent's kill file with tm renamed to tmP (the parent's table; 12 occurrences, all in the simulator and the notations), a new base case, this run's L28 / nus28, and the conjugacy. Everything between (blocks, chain, Lemma T, left word, right-region programs, Lemma S, Inv, inv_step) is verbatim.
• Base case. The simulator from Rc F ([], T0) ([], T0) (= F;; tape0). Record exit 28 was found by a search for the parent's exact record-exit-28 right side [(S1,224495); (S1,673559); (S1,7); (S1,9841); (S1,1942040); (S0,2)] in state B: 18,571,554 simulator steps (parent from A: 18,571,896, the parent's own count; matching only the first one or two runs hits earlier configurations, at about 2.6M and 7.8M steps). 38 pieces: 37 x 500,000 + 71,554.
• Entry into Inv. The chain there has the parent's structure (36 runs, 6 m=3 blocks + block 1 + W_1), so b28_chain is again reflexivity. Gap variables (nearest block first): [18701; 6227; 2069; 683] [233; 8; 9; 8] [12; 1; 0; 0] [0; 0; 0; 0]^3. Difference from the parent: block 2's t gap 936 (x0 = 233) instead of 972 (242), block 3 = (t, s, a, lp) = (52, 8, 1, 5) (x = [12; 1; 0; 0]) instead of (44, 24, 13, 9) ([10; 5; 3; 1]) [corrected in the delta stage below; this line first said (52, 8, 1, 2) / (44, 24, 13, 6)]. Inv (C5, 2, 0, nus28) needs only the window block [18701; 6227; 2069; 683] and 5 deep blocks, so it holds; b28a / b28b are the parent's computations on this L28.
• Conjugacy. perm_sib : Perm (flip tm) tmP phi by case analysis (the only one of the 720 x 2 maps); nonhalt = flip_halts, perm_halts, then nonhalt_P : ~ halts tmP (F;; tape0).
• Validated vs stage 3: the window equals V_r5(1) at record exit 28 and the deep chain differs only by multiples of 4 (stage 3 claims), now exact in Coq.
• Scripts (in W4-3b's rocq/, for both siblings): search3.v (record-exit search), gensib.v (piece configurations), nus.py, parse_out.py, mk_sib.py (assembles both .v files), cfg28s.json, chunks_sib.json, cq.sh. They need W43core.v = the parent's .v lines 26-2233 with \btm\b -> tmP (sed; not kept). The search takes about 25 s, the piece generation 40 s.
• Package (submission/, not posted): the .v (byte-identical), proof.md (delta proof, writeup_lint 0 errors, 0 warnings), parent-proof.md (the parent's write-up), check_kill.txt (local paths as placeholders), README.md, discord.md (one message for both siblings).
• Open: independent re-verification; posting order after the parent (the parent's discord.md says these starts are not formalized; change that sentence or post the sibling message with it).

Delta proof stage, W4-3-sib2 (2026-10-12)

Funded as the delta stage for this sibling of the new kill W4-3 (Class 2 close-out). The .v and its check_kill PASS already existed (stage 2 above). This stage wrote the detailed internal delta proof and its validator.

• Identity re-confirmed: 740 line 588 byte-exact, once; the only map from W4-3's table is sigma = A->B, B->C, C->D, D->E, E->F, F->A with the mirror (720 x 2 searched); start A = sigma(F).
• proof.md (internal, Checkpoint B content), the layout of W4-3b's delta: relation and Lemma R (mirror + relabelling), the opening run in the mirror frame (cell x = this machine's cell -x), the record exits 16-28, record exit 28 in full, C_r5(2) there part by part, the argument, why the runs agree, the formalization delta.
• check_proof.py: SUMMARY PASS 36/36 default, --full adds records to 33 and the parent's S10 (see status.json). The opening run is scripts/rlsim.py (copied unchanged from W4-3b) on this machine's table with L and R swapped, checked cell by cell against tools/sim.py on the unmirrored string (7 step counts to 10^8, and record exit 16 at step 397,796,108). S7 parses proof.md's tables and the public write-up's numbers back and compares them.
• Opening run: lam (mirror frame) set at step 1, small moves at 2, 48-49, 219-220, 6360; 3-cell moves from step 9; record n = (n+1)-th 3-cell move. Record exit 28 at step 2,629,080,059,236 (8,168,172 before the parent's), head on this machine's cell -111,832 in C reading 1. lo = -94, A = -60, B = 111,833, hi = 2,961,776 (mirror frame).
• Against W4-3: at every record exit 12-33 the gap lists differ in exactly five places i, i+1, i+2, i+3, i+7 by -4, -12, -16, +8, -36 (-60 in all), i + 1 per record. All five deep from record exit 26 on; at 16-25 the fifth (the first fossil, 969-973 in W4-3, 36 less here) is still in the window or the right region, so 28 (first of epoch 2) is the right base. At 28: block 5 (inter, digit, sep, sep) = 5, 1, 8, 52 vs 9, 13, 24, 44; block 6's last separator 936 vs 972.
• Error found and fixed: the earlier proof.md / submission/proof.md / submission/README.md gave the two blocks as "936, 36, 37, 34" / "52, 8, 1, 2" against "972, 36, 37, 34" / "44, 24, 13, 6". The fourth entry (lp, the inter gap) was 3 too small everywhere: by the .v's own decoding (lp = 5 + 4 x3) the gaps are 37 / 5 against 37 / 9. Only the prose was wrong; the .v (nus28, L28, cfg28) is right and unchanged (sha256 48b42caf..d1d3). submission/proof.md and README.md corrected (writeup_lint 0/0); S7 now checks the public numbers against the .v.
• Not done: no independent re-run of check_kill (the formalization stage's PASS stands); nothing posted.

Kill

KILLED_NONHALT (2026-10-12). Lemma nonhalt : ~ halts tm c0. in 1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD.v (2,621 lines, Individual62 + stdlib only): the parent W4-3's kill file with its table as tmP, a new base case (init28: F;; tape0 to record exit 28, 38 native_compute pieces, 18,571,554 simulator steps), this run's L28 / nus28, and the conjugacy perm_sib : Perm (flip tm) tmP phi + flip_halts + perm_halts.

• Independent audit: verified (check_kill PASS, exit 0, 2026-10-13T05:11:20Z, on sha256 48b42caf..d1d3). Holdout string at line 624 of the 778 list (byte for byte); whole file read; the reduction chain checked against Flip.v / Permute.v; nonhalt_P diffed against the parent's file (only the base case differs); 0 assumptions.
• Header edit at packaging (comment only): line 35 now says "Informal proof: the accompanying write-up (proof.md), which builds on the parent's write-up." (was "the parent's write-up (proof.md), which covers this start (its base case)"; the audit's one house-style point). diff against the audited file = that one line. New sha256 f9b7173d62f9ec9bfdf3bd0baff3ef0360006a68089b221089fbbbe4939faf9b.
• Fresh check_kill on the final file: PASS, exit 0, 2026-10-13T05:24:36Z, compile 58.9 s (native on), Print Assumptions closed, coqchk timeout at 600 s (policy A warning), integrity PASS. Warning: the second TM_from_str literal (tmP), as expected. Raw output rocq/check_kill_package.out / .log.
• Package submission/ (not posted): the .v (byte-identical to the kill file), proof.md (public delta write-up, rewritten from the internal proof.md: header with viewer link, template and section-to-.v table, summary, sections 1-6 of the mathematics, numerical checks without script names; writeup_lint 0/0), parent-proof.md (the parent's public write-up, byte-identical; lint 0/0), check_kill.txt (this fresh run, local paths as placeholders and the checker's pin/baseline file names in words), README.md (one screen, lint 0/0), discord.md (standalone message with <LINK>, 1,292 characters without the link; post after the parent's message).
• Open: posting (Dennis). The parent's discord.md still says this start is not formalized. The sibling W4-3b's .v header has the same old wording and is not yet independently re-verified.