The rank obstruction behind the preliminary spectral state

The finite catalyst is kept fixed while first tensor powers, then exponent slack, then the number of copies are varied. The hypotheses below isolate the rank inequalities supplied by the catalytic comparison; they do not assert the existence of a tensor spectrum or the separation argument producing that comparison.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_pow_le {K : Type} [Field K] (u j : ℕ) : exactMatrixRank K (u ^ j) ≤ exactMatrixRank K u ^ j

Tensor powers of a fixed exact matrix algorithm retain their exact rank bound after identifying the product coordinates with one matrix dimension.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.floor_rank_power_bounds {u n R : ℕ} (hu : 2 ≤ u) (hn : 1 ≤ n) {τ : ℝ} (hτ : 0 < τ) (hR : ↑R ≤ ↑u ^ τ) (j : ℕ) : have l := ⌊↑j * Real.logb ↑u ↑n / τ⌋₊; ↑R ^ l ≤ ↑n ^ j ∧ ↑n ^ (↑j / τ) ≤ ↑u * ↑u ^ l

A floor approximation uses at most n^j copies of a fixed matrix algorithm and loses at most one factor of its fixed matrix dimension.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.catalytic_rank_bound_at_slack {K : Type} [Field K] {d n Kc R : ℕ} (hd : 0 < d) (hn : 1 ≤ n) (hbound : ∀ (j : ℕ), 1 ≤ j → ∀ (g : ℕ), exactMatrixRank K g ≤ n ^ j → exactMatrixRank K (d ^ j * g) ≤ R * Kc ^ j) {δ : ℝ} (hδ : 0 < δ) : ↑d ^ exactRankExponent K * ↑n ^ (exactRankExponent K / (exactRankExponent K + δ)) ≤ ↑Kc

At fixed n and exponent slack, every admissible matrix rank budget forces the exponential growth rate of the catalytic comparison. The constant R is fixed before the tensor-power parameter varies.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.catalytic_rank_obstruction {K : Type} [Field K] {d k D R : ℕ} (hd : 0 < d) (hbound : ∀ (n : ℕ), 1 ≤ n → ∀ (j : ℕ), 1 ≤ j → ∀ (g : ℕ), exactMatrixRank K g ≤ n ^ j → exactMatrixRank K (d ^ j * g) ≤ R * (n * k + D) ^ j) : ↑d ^ exactRankExponent K ≤ ↑k

The numerical rank consequence of a single fixed finite catalyst is incompatible with k < d^ν. The same D and R occur for every n and every tensor power. No uniform bound on the approximation block selected after an exponent slack is assumed.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.not_catalytic_rank_bounds_of_lt {K : Type} [Field K] {d k D R : ℕ} (hd : 0 < d) (hk : ↑k < ↑d ^ exactRankExponent K) : ¬∀ (n : ℕ), 1 ≤ n → ∀ (j : ℕ), 1 ≤ j → ∀ (g : ℕ), exactMatrixRank K g ≤ n ^ j → exactMatrixRank K (d ^ j * g) ≤ R * (n * k + D) ^ j

Contradiction form for the finite-obstruction argument.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.catalytic_power_comparison {S : Type u_1} [CommSemiring S] [Preorder S] (hadd : ∀ {a b c e : S}, a ≤ b → c ≤ e → a + c ≤ b + e) (hmul : ∀ {a b c e : S}, a ≤ b → c ≤ e → a * c ≤ b * e) (hzero : ∀ (a : S), 0 ≤ a) (D t s : S) (k C : ℕ) (hcat : D + t * s ≤ D + ↑k * s) (hD : D ≤ ↑C * s) (n j : ℕ) : ↑n ^ j * t ^ j * s ≤ ↑(n * k + C) ^ j * s

Iteration and absorption of a fixed catalyst require no cancellation of the tensor factor s. Monotonicity is explicit so the lemma applies to the restriction order on a tensor semiring, where additive cancellation fails.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.catalytic_semiring_obstruction {K : Type} [Field K] {S : Type u_1} [CommSemiring S] [Preorder S] (hadd : ∀ {a b c e : S}, a ≤ b → c ≤ e → a + c ≤ b + e) (hmul : ∀ {a b c e : S}, a ≤ b → c ≤ e → a * c ≤ b * e) (hzero : ∀ (a : S), 0 ≤ a) (ρ : S → ℕ) (hρmono : Monotone ρ) (hρcopies : ∀ (m : ℕ) (s : S), ρ (↑m * s) ≤ m * ρ s) (M : ℕ → S) (hMmul : ∀ (a b : ℕ), M (a * b) = M a * M b) (hMpow : ∀ (a j : ℕ), M (a ^ j) = M a ^ j) (hρM : ∀ (a : ℕ), ρ (M a) = exactMatrixRank K a) (hbudget : ∀ (n j g : ℕ), exactMatrixRank K g ≤ n ^ j → M g ≤ ↑n ^ j) (D s : S) (d k C : ℕ) (hd : 0 < d) (hs : 1 ≤ s) (hcat : D + M d * s ≤ D + ↑k * s) (hD : D ≤ ↑C * s) : ↑d ^ exactRankExponent K ≤ ↑k

A rank-compatible ordered tensor semiring converts a single finite catalytic inequality into the actual exact-rank obstruction. The hypotheses name the required tensor interpretation and scalar rank domination explicitly; no additive rank formula or cancellation property is assumed.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tensor_catalytic_obstruction {K : Type} [Field K] {D s : TensorSemiring.TensorClass K} {d k : ℕ} (hd : 0 < d) (hs : s ≠ 0) (hcat : D + TensorSemiring.matrixClass K d * s ≤ D + ↑k * s) : ↑d ^ exactRankExponent K ≤ ↑k

In the semiring of actual finite tensors over K modulo mutual restriction, a fixed catalyst cannot make k copies dominate multiplication by T_d unless k ≥ d^ν. The nonzero hypothesis is exactly what supplies the scalar restriction s ≥ 1; the catalyst remains fixed throughout.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tensor_catalytic_obstruction_of_scalar_gain {K : Type} [Field K] {D s : TensorSemiring.TensorClass K} {d k m : ℕ} (hd : 0 < d) (hs : s ≠ 0) (hcat : D + ↑m + TensorSemiring.matrixClass K d * s ≤ D + ↑k * s) : ↑d ^ exactRankExponent K ≤ ↑k

The stronger comparison produced by a finite separation certificate has the same consequence. Its positive scalar summand is only needed earlier to rule out s = 0; that nonzero fact is explicit here.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.not_tensor_add_positive_nat_le_self {K : Type} [Field K] (D : TensorSemiring.TensorClass K) {m : ℕ} (hm : 0 < m) : ¬D + ↑m ≤ D

A finite tensor cannot absorb a positive scalar direct summand. Iterating such an absorption would place arbitrarily large scalar tensors below one fixed finite-rank tensor. This uses rank monotonicity, not rank additivity.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tensor_catalytic_obstruction_of_positive_scalar_gain {K : Type} [Field K] {D s : TensorSemiring.TensorClass K} {d k m : ℕ} (hd : 0 < d) (hm : 0 < m) (hcat : D + ↑m + TensorSemiring.matrixClass K d * s ≤ D + ↑k * s) : ↑d ^ exactRankExponent K ≤ ↑k

The exact finite-obstruction comparison from Appendix A.1 forces k ≥ d^ν. Both tensors are fixed, m is a positive scalar gain, and the ordinary tensor rank and restriction order are the actual ones.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.no_tensor_catalytic_gain {K : Type} [Field K] {d k : ℕ} (hd : 0 < d) (hk : ↑k < ↑d ^ exactRankExponent K) : ¬∃ (D : TensorSemiring.TensorClass K) (s : TensorSemiring.TensorClass K) (m : ℕ), 0 < m ∧ D + ↑m + TensorSemiring.matrixClass K d * s ≤ D + ↑k * s

Contradiction interface for the finite inconsistency certificate in the construction of an additive monotone state.