Border substitution for tight tensors

Let T ∈ A ⊗ B ⊗ C with A = ℂ^α. Border substitution lowers the border rank by deleting A-slices: if T has border rank at most r + 1, then projecting A along a suitable line gives border rank at most r. For a tight tensor the line can be taken to be a coordinate axis, so that the projection zeroes one slice. Iterating gives the coordinate-subspace form of Landsberg and Michałek, Towards finding hay in a haystack (Theory of Computing 2025), Proposition 2.3, by a one-parameter-subgroup limit instead of the Borel fixed-point theorem. Here tightness (Tensor3.Tight) asks only the weights on A to be injective, and nonzero slices replace A-conciseness; their restrictions T(q) to coordinate subspaces of A^* are the slice restrictions Tensor3.restrictSlices (see Complexitylib.Algebraic.LinearAlgebra.Tensor.Substitution.Defs).

• Only the kernel matters (Tensor3.BorderRankLE.map_of_ker). If (P ⊗ Y ⊗ Z) T has border rank at most ρ and ker P ⊆ ker P', then so does (P' ⊗ Y ⊗ Z) T, since P' = G P.
• One step (Tensor3.BorderRankLE.exists_map_orthProj). If T has border rank at most r + 1 (and α is nonempty), some u ≠ 0 has (orthProj u ⊗ 1 ⊗ 1) T of border rank at most r, where orthProj u is the orthogonal projection onto u^⊥. No conciseness is assumed.
• Torus limit (Tensor3.Tight.exists_borderRankLE_restrictSlices_erase). If T is tight and (orthProj u ⊗ 1 ⊗ 1) T has border rank at most ρ with u ≠ 0, then for some i in the support of u (the proof uses the one minimizing the weight τA i), T with slice i zeroed has border rank at most ρ.
• One deletion (Tensor3.Tight.exists_mem_borderRankLE_restrictSlices_erase). If T is tight, S is nonempty, and T restricted to the slices in S has border rank at most r + 1, then deleting some i ∈ S leaves border rank at most r.
• Deletion order (Tensor3.Tight.exists_list_borderRankLE_restrictSlices_sdiff). For some ordering l of S₀, deleting the first q elements of l leaves border rank at most r - q (truncated subtraction), for every q. If every slice in S₀ is nonzero, then card S₀ ≤ r (Tensor3.Tight.card_le_of_borderRankLE_restrictSlices), so for a tight tensor all of whose A-slices are nonzero, card α ≤ borderRank T (Tensor3.Tight.card_le_borderRank). In terms of borderRank, q + borderRank T(q) ≤ borderRank T(0) along the ordering (Tensor3.Tight.exists_list_add_borderRank_le), which is Proposition 2.3 for filtrations by coordinate subspaces.
• Lower-bound form (Tensor3.Tight.not_borderRankLE_restrictSlices_of_forall_list). If LB is a lower bound for the border rank of every restriction to a subset of S₀, and every ordering of S₀ has a stage q where q + LB of the surviving slices exceeds r, then the restriction to S₀ does not have border rank at most r.

theorem Algebraic.Tensor3.restrictSlices_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] (T : Tensor3 α β γ) (S : Finset α) (i : α) (j : β) (k : γ) : T.restrictSlices S i j k = if i ∈ S then T i j k else 0

theorem Algebraic.Tensor3.restrictSlices_restrictSlices {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] (T : Tensor3 α β γ) (S S' : Finset α) : (T.restrictSlices S).restrictSlices S' = T.restrictSlices (S' ∩ S)

theorem Algebraic.Tensor3.restrictSlices_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [Fintype α] (T : Tensor3 α β γ) : T.restrictSlices Finset.univ = T

theorem Algebraic.Tensor3.restrictSlices_empty {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] (T : Tensor3 α β γ) : T.restrictSlices ∅ = 0

theorem Algebraic.Tensor3.restrictSlices_eq_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [Fintype α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] (T : Tensor3 α β γ) (S : Finset α) : T.restrictSlices S = map (Matrix.diagonal fun (i : α) => if i ∈ S then 1 else 0) 1 1 T

Restricting to the slices in S is the linear map D ⊗ 1 ⊗ 1 for the diagonal 0/1 matrix D with D i i = 1 exactly when i ∈ S.

theorem Algebraic.Tensor3.BorderRankLE.restrictSlices {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [Fintype α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} {ρ : ℕ} (h : T.BorderRankLE ρ) (S : Finset α) : (T.restrictSlices S).BorderRankLE ρ

Zeroing slices does not increase border rank.

theorem Algebraic.Tensor3.BorderRankLE.restrictSlices_of_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [Fintype α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} {S S' : Finset α} {ρ : ℕ} (h : (T.restrictSlices S).BorderRankLE ρ) (hS : S' ⊆ S) : (T.restrictSlices S').BorderRankLE ρ

Zeroing further slices does not increase border rank.

theorem Algebraic.Tensor3.Tight.restrictSlices {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] {T : Tensor3 α β γ} (hT : T.Tight) (S : Finset α) : (T.restrictSlices S).Tight

Zeroing slices keeps a tensor tight, with the same weights.

theorem Algebraic.Tensor3.orthProj_mulVec {α : Type u_1} [Fintype α] [DecidableEq α] (u v : α → ℂ) : (orthProj u).mulVec v = v - ((star u ⬝ᵥ u)⁻¹ * star u ⬝ᵥ v) • u

theorem Algebraic.Tensor3.orthProj_mulVec_self {α : Type u_1} [Fintype α] [DecidableEq α] (u : α → ℂ) : (orthProj u).mulVec u = 0

theorem Algebraic.Tensor3.orthProj_mulVec_eq_zero_iff {α : Type u_1} [Fintype α] [DecidableEq α] {u v : α → ℂ} : (orthProj u).mulVec v = 0 ↔ ∃ (c : ℂ), v = c • u

The kernel of orthProj u is the line through u.

theorem Algebraic.Tensor3.continuousAt_orthProj {α : Type u_1} [Fintype α] [DecidableEq α] {u : α → ℂ} (hu : u ≠ 0) : ContinuousAt orthProj u

orthProj is continuous away from 0.

theorem Algebraic.Tensor3.BorderRankLE.map_of_ker {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} {α'' : Type u_7} [Fintype α] [Fintype β] [Fintype γ] [Fintype α'] [Fintype β'] [Fintype γ'] {P : Matrix α' α ℂ} {P' : Matrix α'' α ℂ} {Y : Matrix β' β ℂ} {Z : Matrix γ' γ ℂ} {T : Tensor3 α β γ} {ρ : ℕ} (h : (Tensor3.map P Y Z T).BorderRankLE ρ) (hker : ∀ (v : α → ℂ), P.mulVec v = 0 → P'.mulVec v = 0) : (Tensor3.map P' Y Z T).BorderRankLE ρ

Only the kernel matters. If (P ⊗ Y ⊗ Z) T has border rank at most ρ and every vector killed by P is killed by P', then (P' ⊗ Y ⊗ Z) T has border rank at most ρ.

theorem Algebraic.Tensor3.BorderRankLE.exists_map_orthProj {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] [Nonempty α] {T : Tensor3 α β γ} {r : ℕ} (h : T.BorderRankLE (r + 1)) : ∃ (u : α → ℂ), u ≠ 0 ∧ (Tensor3.map (orthProj u) 1 1 T).BorderRankLE r

Border substitution, one step. If T has border rank at most r + 1, then for some u ≠ 0 the projection (orthProj u ⊗ 1 ⊗ 1) T of the first factor onto u^⊥ has border rank at most r.

theorem Algebraic.Tensor3.BorderRankLE.exists_map_orthProj_of_ne_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T ≠ 0) {r : ℕ} (h : T.BorderRankLE (r + 1)) : ∃ (u : α → ℂ), u ≠ 0 ∧ (Tensor3.map (orthProj u) 1 1 T).BorderRankLE r

Border substitution, one step, for a nonzero tensor.

theorem Algebraic.Tensor3.Tight.exists_borderRankLE_restrictSlices_erase {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) {u : α → ℂ} (hu : u ≠ 0) {ρ : ℕ} (h : (map (orthProj u) 1 1 T).BorderRankLE ρ) : ∃ (i : α), u i ≠ 0 ∧ (T.restrictSlices (Finset.univ.erase i)).BorderRankLE ρ

The torus limit. If T is tight and its projection along u ≠ 0 has border rank at most ρ, then for some i in the support of u, T with the slice i zeroed has border rank at most ρ. (The proof takes the i minimizing τA on the support of u.)

theorem Algebraic.Tensor3.Tight.exists_mem_borderRankLE_restrictSlices_erase {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) {S : Finset α} (hS : S.Nonempty) {r : ℕ} (h : (T.restrictSlices S).BorderRankLE (r + 1)) : ∃ i ∈ S, (T.restrictSlices (S.erase i)).BorderRankLE r

Border substitution for tight tensors, one deletion. If T is tight, S is nonempty, and T restricted to the slices in S has border rank at most r + 1, then for some i ∈ S, T restricted to the slices in S \ {i} has border rank at most r.

theorem Algebraic.Tensor3.Tight.exists_list_borderRankLE_restrictSlices_sdiff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) (S₀ : Finset α) {r : ℕ} (h : (T.restrictSlices S₀).BorderRankLE r) : ∃ (l : List α), l.Nodup ∧ l.toFinset = S₀ ∧ ∀ (q : ℕ), (T.restrictSlices (S₀ \ (List.take q l).toFinset)).BorderRankLE (r - q)

Border substitution for tight tensors, deletion order. If T is tight and T restricted to the slices in S₀ has border rank at most r, then some ordering l of S₀ (l.Nodup and l.toFinset = S₀) has the property that, for every q, deleting the first q elements of l from S₀ leaves a restriction of border rank at most r - q.

theorem Algebraic.Tensor3.Tight.card_le_of_borderRankLE_restrictSlices {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) {S : Finset α} (hS : ∀ i ∈ S, T i ≠ 0) {r : ℕ} (h : (T.restrictSlices S).BorderRankLE r) : S.card ≤ r

A tight tensor restricted to S nonzero slices has border rank at least card S.

theorem Algebraic.Tensor3.Tight.card_le_borderRank {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) (h : ∀ (i : α), T i ≠ 0) : Fintype.card α ≤ T.borderRank

A tight tensor all of whose A-slices are nonzero has border rank at least card α.

theorem Algebraic.Tensor3.Tight.exists_list_add_borderRank_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) {S₀ : Finset α} (hS : ∀ i ∈ S₀, T i ≠ 0) : ∃ (l : List α), l.Nodup ∧ l.toFinset = S₀ ∧ ∀ q ≤ S₀.card, q + (T.restrictSlices (S₀ \ (List.take q l).toFinset)).borderRank ≤ (T.restrictSlices S₀).borderRank

Border substitution for tight tensors, filtration form (the coordinate form of Landsberg and Michałek, Proposition 2.3). If T is tight and every slice in S₀ is nonzero, then some ordering l of S₀ satisfies q + borderRank T(q) ≤ borderRank T(0) for every q ≤ card S₀, where T(q) is T restricted to S₀ minus the first q elements of l.

theorem Algebraic.Tensor3.Tight.not_borderRankLE_restrictSlices_of_forall_list {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) {S₀ : Finset α} (hS : ∀ i ∈ S₀, T i ≠ 0) {r : ℕ} (LB : Finset α → ℕ) (hLB : ∀ S ⊆ S₀, ∀ (ρ : ℕ), (T.restrictSlices S).BorderRankLE ρ → LB S ≤ ρ) (h : ∀ (l : List α), l.Nodup → l.toFinset = S₀ → ∃ q ≤ S₀.card, r < q + LB (S₀ \ (List.take q l).toFinset)) : ¬(T.restrictSlices S₀).BorderRankLE r

Border substitution for tight tensors, lower-bound form. Let T be tight with every slice in S₀ nonzero, and let LB S be a lower bound for the border rank of T restricted to any S ⊆ S₀. If for every ordering l of S₀ some stage q ≤ card S₀ has r < q + LB (S₀ \ {first q elements of l}), then T restricted to S₀ does not have border rank at most r.