The explicit border-rank lower bound: proof internals

Proofs behind Complexitylib.Algebraic.LinearAlgebra.Tensor.Explicit.

• Tightness. weightedLMTensor k is supported on ℓ = j + (a - k), so the weights a - k, j, -ℓ make it tight. Slice a has the nonzero entry 2^{2^{…}} at j = k - a, ℓ = 0 if a ≤ k, and at j = 0, ℓ = a - k otherwise.
• Greedy distinct subset sums. The invariant is NoSignedRelation x: no nontrivial combination ∑ ε_t x_t with ε_t ∈ {-1, 0, 1} vanishes, which is equivalent to all subset sums being distinct. The signed sums ∑ ε_t x_t of i chosen elements number at most 3^i, so a set A with more than 3^i elements has an element a outside them; a relation with coefficient ±1 on a would put a among the signed sums, so prepending a keeps the invariant. After n + 1 steps, sorting the chosen set gives a strictly increasing tuple; its subset sums are subset sums of the chosen set, which are distinct.
• Clusters in blocks. Applying the greedy step to the offsets a - k of the slices of a set B gives a strictly increasing cluster in B with distinct subset sums of offsets. In a block of length L the offsets lie in an interval of L consecutive integers, so the diameter is at most L - 1, and the signs of the offsets are those of the block.
• The paired-cluster hypothesis. For good blocks B⁺ and B⁻, the greedy clusters satisfy the conditions of PairedKoszulBound, and their medians a = c⁺ p ∈ B⁺, b = c⁻ p ∈ B⁻ witness DeletionGame.PairedClusterBound with D = (2p + 1) / (p + 1) and R ≥ 3^{2p} + 1.
• Arithmetic. 1 + 2D/3 = 7/3 - 2 / (3 (p + 1)), and D ≥ 3/2 iff p ≥ 1. For the asymptotic form choose L ≥ 2 R / δ, so that R m / L ≤ δ m / 2, and then k so large that the constant D E + 8 L + 2 is at most δ m / 2.
• The unconditional bounds. The paired-cluster certificate Tensor3.div_mul_phi_sub_le_borderRank_restrictSlices is PairedKoszulBound k p L E with E = 8 (p + 1) L, for all k, p, L; then D E = 8 (2p + 1) L.

Tightness

theorem Algebraic.Tensor3.Internal.Explicit.lmTensor_apply (k : ℕ) (γ : Fin (2 * k + 1) → Fin (2 * k + 1) → ℂ) (a j l : Fin (2 * k + 1)) : lmTensor k γ a j l = if ↑↑l = ↑↑j + (↑↑a - ↑k) then γ a j else 0

theorem Algebraic.Tensor3.Internal.Explicit.lmWeight_ne_zero (k : ℕ) (a j : Fin (2 * k + 1)) : lmWeight k a j ≠ 0

theorem Algebraic.Tensor3.Internal.Explicit.tight_lmTensor (k : ℕ) (γ : Fin (2 * k + 1) → Fin (2 * k + 1) → ℂ) : (lmTensor k γ).Tight

theorem Algebraic.Tensor3.Internal.Explicit.lmTensor_ne_zero (k : ℕ) {γ : Fin (2 * k + 1) → Fin (2 * k + 1) → ℂ} (hγ : ∀ (a j : Fin (2 * k + 1)), γ a j ≠ 0) (a : Fin (2 * k + 1)) : lmTensor k γ a ≠ 0

theorem Algebraic.Tensor3.Internal.Explicit.tight_weightedLMTensor (k : ℕ) : (weightedLMTensor k).Tight

theorem Algebraic.Tensor3.Internal.Explicit.weightedLMTensor_ne_zero (k : ℕ) (a : Fin (2 * k + 1)) : weightedLMTensor k a ≠ 0

Greedy distinct subset sums

def Algebraic.Tensor3.Internal.Explicit.NoSignedRelation {n : ℕ} (x : Fin n → ℤ) : Prop

No nontrivial combination of the x t with coefficients in {-1, 0, 1} vanishes.

Equations

• Algebraic.Tensor3.Internal.Explicit.NoSignedRelation x = ∀ (ε : Fin n → ℤ), (∀ (t : Fin n), ε t ∈ {-1, 0, 1}) → ∑ t : Fin n, ε t * x t = 0 → ∀ (t : Fin n), ε t = 0

def Algebraic.Tensor3.Internal.Explicit.signedSums {n : ℕ} (x : Fin n → ℤ) : Finset ℤ

The signed sums ∑ ε_t x_t with coefficients ε_t ∈ {-1, 0, 1}.

Equations

• Algebraic.Tensor3.Internal.Explicit.signedSums x = Finset.image (fun (ε : Fin n → ℤ) => ∑ t : Fin n, ε t * x t) (Fintype.piFinset fun (x : Fin n) => {-1, 0, 1})

theorem Algebraic.Tensor3.Internal.Explicit.card_signedSums_le {n : ℕ} (x : Fin n → ℤ) : (signedSums x).card ≤ 3 ^ n

theorem Algebraic.Tensor3.Internal.Explicit.neg_mem_signedCoeffs {e : ℤ} (he : e ∈ {-1, 0, 1}) : -e ∈ {-1, 0, 1}

theorem Algebraic.Tensor3.Internal.Explicit.noSignedRelation_cons {n : ℕ} {x : Fin n → ℤ} (hx : NoSignedRelation x) {a : ℤ} (ha : a ∉ signedSums x) : NoSignedRelation (Fin.cons a x)

theorem Algebraic.Tensor3.Internal.Explicit.exists_noSignedRelation (A : Finset ℤ) {m : ℕ} (hA : 3 ^ m < A.card) (i : ℕ) : i ≤ m + 1 → ∃ (x : Fin i → ℤ), (∀ (t : Fin i), x t ∈ A) ∧ NoSignedRelation x

theorem Algebraic.Tensor3.Internal.Explicit.sum_injective_of_noSignedRelation {n : ℕ} {x : Fin n → ℤ} (hx : NoSignedRelation x) : Function.Injective fun (I : Finset (Fin n)) => ∑ t ∈ I, x t

theorem Algebraic.Tensor3.Internal.Explicit.exists_strictMono_injective_sum (A : Finset ℤ) {n : ℕ} (hA : 3 ^ n < A.card) : ∃ (x : Fin (n + 1) → ℤ), StrictMono x ∧ (∀ (t : Fin (n + 1)), x t ∈ A) ∧ Function.Injective fun (I : Finset (Fin (n + 1))) => ∑ t ∈ I, x t

Clusters in blocks

theorem Algebraic.Tensor3.Internal.Explicit.exists_cluster {k p : ℕ} (B : Finset (Fin (2 * k + 1))) (hB : 3 ^ (2 * p) + 1 ≤ B.card) : ∃ (c : Fin (2 * p + 1) → Fin (2 * k + 1)), StrictMono c ∧ (∀ (t : Fin (2 * p + 1)), c t ∈ B) ∧ Function.Injective fun (I : Finset (Fin (2 * p + 1))) => ∑ t ∈ I, clusterOffsets k c t

theorem Algebraic.Tensor3.Internal.Explicit.mem_posBlock {k L i : ℕ} {a : Fin (2 * k + 1)} : a ∈ DeletionGame.posBlock k L i ↔ ↑i * ↑L + 1 ≤ DeletionGame.offset k a ∧ DeletionGame.offset k a ≤ (↑i + 1) * ↑L

theorem Algebraic.Tensor3.Internal.Explicit.mem_negBlock {k L i : ℕ} {a : Fin (2 * k + 1)} : a ∈ DeletionGame.negBlock k L i ↔ ↑i * ↑L + 1 ≤ -DeletionGame.offset k a ∧ -DeletionGame.offset k a ≤ (↑i + 1) * ↑L

theorem Algebraic.Tensor3.Internal.Explicit.exists_cluster_posBlock {k p : ℕ} (S : Finset (Fin (2 * k + 1))) {L i : ℕ} (hS : 3 ^ (2 * p) + 1 ≤ (S ∩ DeletionGame.posBlock k L i).card) : ∃ (c : Fin (2 * p + 1) → Fin (2 * k + 1)), StrictMono c ∧ (∀ (t : Fin (2 * p + 1)), c t ∈ S ∩ DeletionGame.posBlock k L i) ∧ (Function.Injective fun (I : Finset (Fin (2 * p + 1))) => ∑ t ∈ I, clusterOffsets k c t) ∧ clusterOffsets k c (Fin.last (2 * p)) - clusterOffsets k c 0 ≤ ↑L - 1 ∧ ∀ (t : Fin (2 * p + 1)), 1 ≤ clusterOffsets k c t ∧ clusterOffsets k c t ≤ ↑k

theorem Algebraic.Tensor3.Internal.Explicit.exists_cluster_negBlock {k p : ℕ} (S : Finset (Fin (2 * k + 1))) {L i : ℕ} (hS : 3 ^ (2 * p) + 1 ≤ (S ∩ DeletionGame.negBlock k L i).card) : ∃ (c : Fin (2 * p + 1) → Fin (2 * k + 1)), StrictMono c ∧ (∀ (t : Fin (2 * p + 1)), c t ∈ S ∩ DeletionGame.negBlock k L i) ∧ (Function.Injective fun (I : Finset (Fin (2 * p + 1))) => ∑ t ∈ I, clusterOffsets k c t) ∧ clusterOffsets k c (Fin.last (2 * p)) - clusterOffsets k c 0 ≤ ↑L - 1 ∧ ∀ (t : Fin (2 * p + 1)), -↑k ≤ clusterOffsets k c t ∧ clusterOffsets k c t ≤ -1

The paired-cluster hypothesis

theorem Algebraic.Tensor3.Internal.Explicit.pairedClusterBound_on {k p : ℕ} {β : Type u_1} {γ : Type u_2} {T : Tensor3 (Fin (2 * k + 1)) β γ} {L R : ℕ} {E : ℝ} (h : T.PairedKoszulBoundOn p L E) (hR : 3 ^ (2 * p) + 1 ≤ R) : DeletionGame.PairedClusterBound k L R ((2 * ↑p + 1) / (↑p + 1)) E fun (S : Finset (Fin (2 * k + 1))) => (T.restrictSlices S).borderRank

theorem Algebraic.Tensor3.Internal.Explicit.pairedClusterBound {k p L R : ℕ} {E : ℝ} (h : PairedKoszulBound k p L E) (hR : 3 ^ (2 * p) + 1 ≤ R) : DeletionGame.PairedClusterBound k L R ((2 * ↑p + 1) / (↑p + 1)) E fun (S : Finset (Fin (2 * k + 1))) => ((weightedLMTensor k).restrictSlices S).borderRank

Arithmetic

theorem Algebraic.Tensor3.Internal.Explicit.three_div_two_le {p : ℕ} (hp : 1 ≤ p) : 3 / 2 ≤ (2 * ↑p + 1) / (↑p + 1)

theorem Algebraic.Tensor3.Internal.Explicit.one_add_two_mul_div_three (p : ℕ) : 1 + 2 * ((2 * ↑p + 1) / (↑p + 1)) / 3 = 7 / 3 - 2 / (3 * (↑p + 1))

theorem Algebraic.Tensor3.Internal.Explicit.eventually_sub_mul_le_of_le {f : ℕ → ℝ} {c C δ : ℝ} {R L : ℕ} (hδ : 0 < δ) (hL0 : 0 < L) (hLR : 2 * ↑R / δ ≤ ↑L) (h : ∀ᶠ (k : ℕ) in Filter.atTop, c * (2 * ↑k + 1) - C - ↑R * (2 * ↑k + 1) / ↑L ≤ f k) : ∀ᶠ (k : ℕ) in Filter.atTop, (c - δ) * (2 * ↑k + 1) ≤ f k

For L ≥ 2 R / δ, a lower bound c m - C - R m / L with a constant C gives (c - δ) m for all large k, where m = 2k + 1.

theorem Algebraic.Tensor3.Internal.Explicit.exists_blockLength (p : ℕ) (δ : ℝ) : ∃ (L : ℕ), 3 ^ (2 * p) + 1 ≤ L ∧ 2 * (3 ^ (2 * p) + 1) / δ ≤ ↑L

A block length L ≥ 3^{2p} + 1 with 2 (3^{2p} + 1) / δ ≤ L.

theorem Algebraic.Tensor3.Internal.Explicit.le_borderRank_of_pairedKoszulBoundOn {k p : ℕ} {β : Type u_1} {γ : Type u_2} [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 (Fin (2 * k + 1)) β γ} (hT : T.Tight) (hT0 : ∀ (i : Fin (2 * k + 1)), T i ≠ 0) {L : ℕ} {E : ℝ} (h : T.PairedKoszulBoundOn p L E) (hp : 1 ≤ p) (hL : 3 ^ (2 * p) + 1 ≤ L) (hLk : L ≤ k) : (7 / 3 - 2 / (3 * (↑p + 1))) * (2 * ↑k + 1) - (2 * ↑p + 1) / (↑p + 1) * E - (8 * ↑L + (3 ^ (2 * p) + 1) * (2 * ↑k + 1) / ↑L + 2) ≤ ↑T.borderRank

theorem Algebraic.Tensor3.Internal.Explicit.le_borderRank_of_pairedKoszulBoundOn_eight {k p : ℕ} {β : Type u_1} {γ : Type u_2} [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 (Fin (2 * k + 1)) β γ} (hT : T.Tight) (hT0 : ∀ (i : Fin (2 * k + 1)), T i ≠ 0) {L : ℕ} (h : T.PairedKoszulBoundOn p L (8 * (↑p + 1) * ↑L)) (hp : 1 ≤ p) (hL : 3 ^ (2 * p) + 1 ≤ L) (hLk : L ≤ k) : (7 / 3 - 2 / (3 * (↑p + 1))) * (2 * ↑k + 1) - (16 * (↑p + 1) * ↑L + (3 ^ (2 * p) + 1) * (2 * ↑k + 1) / ↑L + 2) ≤ ↑T.borderRank

The finite bound with E = 8 (p + 1) L, where D E + 8 L = 16 (p + 1) L.

theorem Algebraic.Tensor3.Internal.Explicit.eventually_le_borderRank_of_pairedKoszulBoundOn {p : ℕ} {T : (k : ℕ) → Tensor3 (Fin (2 * k + 1)) (Fin (2 * k + 1)) (Fin (2 * k + 1))} (hT : ∀ (k : ℕ), (T k).Tight) (hT0 : ∀ (k : ℕ) (i : Fin (2 * k + 1)), T k i ≠ 0) (hp : 1 ≤ p) {δ : ℝ} (hδ : 0 < δ) {L : ℕ} (hL : 3 ^ (2 * p) + 1 ≤ L) (hLδ : 2 * (3 ^ (2 * p) + 1) / δ ≤ ↑L) (h : ∀ᶠ (k : ℕ) in Filter.atTop, (T k).PairedKoszulBoundOn p L (8 * (↑p + 1) * ↑L)) : ∀ᶠ (k : ℕ) in Filter.atTop, (7 / 3 - 2 / (3 * (↑p + 1)) - δ) * (2 * ↑k + 1) ≤ ↑(T k).borderRank

The asymptotic bound for a family. If tight tensors T k with nonzero slices satisfy PairedKoszulBoundOn (T k) p L (8 (p + 1) L) for all large k, for one block length L with 3^{2p} + 1 ≤ L and 2 (3^{2p} + 1) / δ ≤ L, then borderRank (T k) ≥ (7/3 - 2 / (3 (p + 1)) - δ) (2k + 1) for all large k.

The unconditional bounds

theorem Algebraic.Tensor3.Internal.Explicit.le_borderRank_of_pairedKoszulBound {k p L : ℕ} {E : ℝ} (h : PairedKoszulBound k p L E) (hp : 1 ≤ p) (hL : 3 ^ (2 * p) + 1 ≤ L) (hLk : L ≤ k) : (7 / 3 - 2 / (3 * (↑p + 1))) * (2 * ↑k + 1) - (2 * ↑p + 1) / (↑p + 1) * E - (8 * ↑L + (3 ^ (2 * p) + 1) * (2 * ↑k + 1) / ↑L + 2) ≤ ↑(weightedLMTensor k).borderRank

theorem Algebraic.Tensor3.Internal.Explicit.pairedKoszulBound (k p L : ℕ) : PairedKoszulBound k p L (8 * (↑p + 1) * ↑L)

theorem Algebraic.Tensor3.Internal.Explicit.le_borderRank {k p L : ℕ} (hp : 1 ≤ p) (hL : 3 ^ (2 * p) + 1 ≤ L) (hLk : L ≤ k) : (7 / 3 - 2 / (3 * (↑p + 1))) * (2 * ↑k + 1) - (16 * (↑p + 1) * ↑L + (3 ^ (2 * p) + 1) * (2 * ↑k + 1) / ↑L + 2) ≤ ↑(weightedLMTensor k).borderRank

theorem Algebraic.Tensor3.Internal.Explicit.eventually_le_borderRank {p : ℕ} (hp : 1 ≤ p) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (k : ℕ) in Filter.atTop, (7 / 3 - 2 / (3 * (↑p + 1)) - δ) * (2 * ↑k + 1) ≤ ↑(weightedLMTensor k).borderRank

theorem Algebraic.Tensor3.Internal.Explicit.eventually_nineteen_div_nine {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (k : ℕ) in Filter.atTop, (19 / 9 - δ) * (2 * ↑k + 1) ≤ ↑(weightedLMTensor k).borderRank

theorem Algebraic.Tensor3.Internal.Explicit.eventually_twentyOne_div_ten : ∀ᶠ (k : ℕ) in Filter.atTop, 21 / 10 * (2 * ↑k + 1) ≤ ↑(weightedLMTensor k).borderRank

theorem Algebraic.Tensor3.Internal.Explicit.exists_two_div_lt {ε : ℝ} (hε : 0 < ε) : ∃ (p : ℕ), 1 ≤ p ∧ 2 / (3 * (↑p + 1)) < ε

For ε > 0, some p ≥ 1 has 2 / (3 (p + 1)) < ε.

theorem Algebraic.Tensor3.Internal.Explicit.eventually_seven_div_three {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (k : ℕ) in Filter.atTop, (7 / 3 - ε) * (2 * ↑k + 1) ≤ ↑(weightedLMTensor k).borderRank