From exact tensor rank to arithmetic complexity

This file supplies the arithmetic conversion in Section 6.2, over an arbitrary field F. It uses the division-free straight-line programs of MatrixMultiplication.Arithmetic: loading inputs and constants is free, and each scalar addition, subtraction, or multiplication costs one. Correctness means matrix multiplication on every pair of inputs.

The block recursion is the field-generic one of Arithmetic.rectangularAdmissibleExponent_of_rankAtMost (with aspect k = 1). The substantive tensor estimates are separate: any family of exact decompositions of ⟨n,n,n⟩ over F with ranks ≤ n^(τ+δ) for every δ > 0 gives omega F ≤ τ. In particular omega K ≤ exactRankExponent K.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.admissibleExponent_of_rankAtMost {F : Type u_1} [Field F] {n R : ℕ} (hn : 2 ≤ n) (hRank : (Foundation.Tensor.matMul F n n n).RankAtMost R) {τ : ℝ} (hτ : 2 ≤ τ) (hR : ↑R ≤ ↑n ^ τ) : Arithmetic.AdmissibleExponent F τ

A finite exact decomposition over F gives an arithmetic bound over F by block substitution, including all the scalar operations in the linear combinations, followed by padding to arbitrary positive sizes.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.omega_le_of_rankAtMost {F : Type u_1} [Field F] {n R : ℕ} (hn : 2 ≤ n) (hRank : (Foundation.Tensor.matMul F n n n).RankAtMost R) {τ : ℝ} (hτ : 2 ≤ τ) (hR : ↑R ≤ ↑n ^ τ) : Arithmetic.omega F ≤ τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.omega_le_of_arbitrarily_close_rankBounds {F : Type u_1} [Field F] {τ : ℝ} (hτ : 2 ≤ τ) (hRank : ∀ (δ : ℝ), 0 < δ → ∃ (n : ℕ) (R : ℕ), 2 ≤ n ∧ (Foundation.Tensor.matMul F n n n).RankAtMost R ∧ ↑R ≤ ↑n ^ (τ + δ)) : Arithmetic.omega F ≤ τ

Near-optimal finite blocks suffice: no finite decomposition is required to attain the limiting exponent.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.omega_le_exactRankExponent {K : Type} [Field K] : Arithmetic.omega K ≤ exactRankExponent K

General exact-rank-to-arithmetic bridge. The proof uses a lower bound for every finite-block exponent, so it does not require attainment of the infimum.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.arithmeticComplexity_of_exactRankExponent_le {K : Type} [Field K] {τ : ℝ} (hτ : exactRankExponent K ≤ τ) (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∃ (P : Arithmetic.MatrixAlgorithm K n n n), P.Correct ∧ ↑P.cost ≤ C * ↑n ^ (τ + ε)

Explicit epsilon-complexity conclusion from an exact-rank exponent bound.