A single integer-entry tensor family of border rank (7/3-o(1)) m

The computable family Dissociated.tensor m is independent of epsilon, is defined at every dimension by zero padding an odd core, and has coefficient binary length at most m+1. Its complex border rank is eventually at least (7/3-ε)m for every positive epsilon. In particular it eventually has border rank at least 17m/8.

This uniformizes the checked periodic paired-cluster construction. The motivating research note, Distinct subset sums and explicit tensor border rank, Revision 2, uses the same dissociated-cluster and periodic coefficient ideas to approach 17/8. Here the existing stronger paired-cluster proof replaces its five-far-diagonal branch. All tensor-theoretic inputs are proved in the library: substitution, Koszul flattenings, block nonsingularity, and the deletion game.

The entry formula and bounded parameter search are computable, and their binary output size is polynomial. A polynomial-time machine implementation is not proved by these declarations; output-size bounds alone do not certify running time.

theorem Algebraic.Tensor3.Dissociated.order_le_log (k : ℕ) : order k ≤ Nat.log 2 (2 * k + 1)

The order search never exceeds the binary logarithm of the odd core dimension.

theorem Algebraic.Tensor3.Dissociated.card_candidates_le (k : ℕ) : (candidates k).card ≤ Nat.log 2 (2 * k + 1) + 1

The admissible candidate set has at most logarithmically many elements.

theorem Algebraic.Tensor3.Dissociated.eventually_admissible {p : ℕ} (hp : 1 ≤ p) : ∀ᶠ (k : ℕ) in Filter.atTop, Admissible k p

Every fixed positive order eventually becomes admissible in the uniform search.

theorem Algebraic.Tensor3.Dissociated.order_tendsto : Filter.Tendsto order Filter.atTop Filter.atTop

The selected cluster order tends to infinity.

theorem Algebraic.Tensor3.Dissociated.odd_lowerBound_of_admissible {k : ℕ} (hk : Admissible k (order k)) : (7 / 3 - 8 / (3 * (↑(order k) + 1))) * (2 * ↑k + 1) ≤ ↑(oddTensor k).borderRank

The finite rank guarantee once the selected order passes the construction's checks.

theorem Algebraic.Tensor3.Dissociated.entry_size_le (m : ℕ) (a j l : Fin m) : (entry m ↑a ↑j ↑l).size ≤ m + 1

Every valid tensor coefficient has at most m+1 binary digits.

theorem Algebraic.Tensor3.Dissociated.tensor_entry (m : ℕ) (a j l : Fin m) : ∃ (v : ℕ), v.size ≤ m + 1 ∧ tensor m a j l = ↑v

Every coordinate is a nonnegative integer with the stated binary-size bound.

theorem Algebraic.Tensor3.Dissociated.sum_entry_size_le (m : ℕ) : ∑ a : Fin m, ∑ j : Fin m, ∑ l : Fin m, (entry m ↑a ↑j ↑l).size ≤ m ^ 3 * (m + 1)

The dense coordinate array has polynomial total binary output size.

theorem Algebraic.Tensor3.Dissociated.eventually_sub_mul_le_borderRank {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (m : ℕ) in Filter.atTop, (7 / 3 - ε) * ↑m ≤ ↑(tensor m).borderRank

The same computable family has border rank (7/3-o(1))m at all dimensions.

theorem Algebraic.Tensor3.Dissociated.eventually_seventeen_div_eight_mul_le_borderRank : ∀ᶠ (m : ℕ) in Filter.atTop, 17 / 8 * ↑m ≤ ↑(tensor m).borderRank

In particular the single integer-entry family eventually exceeds the note's 17/8 target.