W4-3b 1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---

740 line 512 (778 line 543). 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->B, B->C, C->D, D->E, E->A, F->F, no mirror (12/12 entries; the only map). It starts in A = the parent's B, so it runs the parent's table from 0^inf B> 0^inf. 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 1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---.v (2,621 lines, sha256 ef701290..2296, Individual62 + stdlib only). check_kill: PASS, compile 71.96 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 B ([], T0) ([], T0) (= B;; 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,902 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,902.
• 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] [242; 8; 9; 8] [10; 5; 4; 1] [0; 0; 0; 0]^3. Difference from the parent: block 3's digit gap a: x2 = 4 (gap 17) instead of the parent's 3 (gap 13); everything else equal. 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 tm tmP phi by case analysis (the only one of the 720 x 2 maps); nonhalt = perm_halts, then nonhalt_P : ~ halts tmP (B;; 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).
• Concurrent work: another session wrote this directory's proof.md (a longer internal delta proof), check_proof.py, check_proof.out and scripts/rlsim.py from 21:12 on, around this .v. This stage did not touch those files; its own short public delta is submission/proof.md.
• 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 (workflow name W4-3-sib1, 2026-10-12)

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. Ran in parallel with the formalization stage above; this stage wrote only proof.md, check_proof.py, check_proof.out, check_proof_full.out and scripts/rlsim.py (and merged two fields into status.json). It did not touch the .v, rocq/ or submission/.

Result: proof.md complete and validated (Checkpoint B content). check_proof.py 30/30 PASS (44 s), --full 32/32.

• Relation. Line 512 of the 740 list byte-exact and once; sheet row class only, no claim. sigma = parent -> here EABCDF, no mirror, the only map of 720 x 2; start = sigma(B). Lockstep with the parent's table from B for 2e6 steps (Python) and the same tape at 1e9 (tools/sim.py C engine).
• Opening run, independently. New scripts/rlsim.py: run-length simulator of a 2-symbol table (alternating segments on two stacks, one move per segment when (state, near symbol) is in a sweep cycle; cycles found from the table, not hard-coded). Validated against tools/sim.py at 7 step counts to 1e8 (whole tape) and on lam for 2e6 steps. It runs THIS machine's own table, not the renamed one. To record exit 28: 18.8M iterations, 16 s.
• Records. lam small moves here: 1, 4-5, 18-19, 930-931, 7984, 17719-17720 (parent: 1, 6-7, 838-839, 7820, 17531-17532); no extra start-up 3-cell move, so record n = n-th 3-cell move as in the parent (588 differs). The operational record exits 12..33 (parent 3.3 definition, K = K0(r)+2e also for e = -1) land exactly on the parent's defect-model snapshot steps (snap_512.pkl), for this start and for the parent's own run (snap_341.pkl). Record exit 28: step 2,629,088,387,088, head cell 111,896 (parent: 2,629,088,227,408, 111,894).
• Invariant. Own reading of P§3.3 (not the parent's window.py): (L), (C), (H) at 16..28 (16..33 --full) for both runs; at 28 (W) = V_r5(1), with V parsed from the parent's submission/proof.md table. --full: C_r(2) with V_r(1) at every record exit 28..33 (all six classes).
• The difference. At every record exit 12..33 the gap lists (lo -> defects -> hi) differ in exactly one entry, +4 here, index +1 per record (gap 10 from lo at record 12; digit gap of block 2 at 16; digit gap of block 5 at 28: 17 vs 13). Same K, window and right region at 16..33. So the start-up windows 16..27 are the parent's Appendix C values.
• Formal data tie-in (S5). The .v's cfg28 expands cell for cell to the rlsim tape at record exit 28 (both sides), the parent's cfg28 likewise for the parent; L28/nus28 decode; only nus28 block 3 (= block 5 from the left) differs. Library (2,202 lines) and inv28..base28 (45 lines) = the parent's text with tm -> tmP; 38 pieces = 18,571,902 simulator steps. This matches the formalization stage's numbers above.
• writeup_lint on proof.md: 6 errors (repo paths, scripts, the word checkpoint), 1 inline-formula warning. Expected: this is the internal proof; the public delta is the formalization stage's submission/proof.md.
• Open: Dennis's Checkpoint B read (non-blocking); independent re-run of check_kill (formalization stage's next).