Uniform periodic tensor estimates

The checked paired-cluster lower bound supplies the rank estimate; a finite search chooses all parameters uniformly while keeping every coefficient's binary length linear.

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

Every fixed positive order eventually passes all finite checks.

theorem Algebraic.Tensor3.Dissociated.Internal.mem_candidates {k p : ℕ} (hp : Admissible k p) : p ∈ candidates k

An admissible order is present in the actual bounded search.

theorem Algebraic.Tensor3.Dissociated.Internal.le_order {k p : ℕ} (hp : Admissible k p) : p ≤ order k

The chosen order is at least any admissible order.

theorem Algebraic.Tensor3.Dissociated.Internal.admissible_order {k p : ℕ} (hp : Admissible k p) : Admissible k (order k)

If any order is admissible, the maximal selected order is admissible.

theorem Algebraic.Tensor3.Dissociated.Internal.eventually_le_order (p : ℕ) : ∀ᶠ (k : ℕ) in Filter.atTop, p ≤ order k

The selected orders tend to infinity; the tensor does not depend on epsilon.

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

The selected order always lies in the logarithmic search range.

theorem Algebraic.Tensor3.Dissociated.Internal.oddTensor_eq {k : ℕ} (hk : Admissible k (order k)) : oddTensor k = periodicLMTensor k (rowPeriod (order k)) (columnPeriod (order k))

Above the cutoff the tensor is exactly an existing periodic tensor.

theorem Algebraic.Tensor3.Dissociated.Internal.oddEntry_size_le (k a j l : ℕ) : (oddEntry k a j l).size ≤ 2 * k + 2

Every integer coefficient has at most the dimension plus one binary digits.

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

The finite lower bound of the uniformly selected tensor.

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

The one odd-dimensional family approaches the paired-cluster coefficient.

theorem Algebraic.Tensor3.Dissociated.Internal.core_bounds {m : ℕ} (hm : 0 < m) : 2 * coreIndex m + 1 ≤ m ∧ m ≤ 2 * coreIndex m + 2

The padded core loses at most one dimension.

theorem Algebraic.Tensor3.Dissociated.Internal.entry_size_le {m a : ℕ} (ha : a < m) (j l : ℕ) : (entry m a j l).size ≤ m + 1

Each valid coordinate has a linear bound on its binary output size.

theorem Algebraic.Tensor3.Dissociated.Internal.odd_borderRank_le {m : ℕ} (hm : 0 < m) : (oddTensor (coreIndex m)).borderRank ≤ (tensor m).borderRank

Coordinate restriction recovers the whole odd core exactly.

theorem Algebraic.Tensor3.Dissociated.Internal.coreIndex_tendsto : Filter.Tendsto coreIndex Filter.atTop Filter.atTop

Growing ambient dimension also grows the odd core.

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

Padding preserves the limiting coefficient, with an explicit small epsilon guard.

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

A single family, independent of epsilon, attains coefficient 7/3-o(1).