Integer rounding in the detecting-character argument

The character used at a matrix size may depend on that size. A uniform bound on all those characters is enough: the loss of one in rounding their target values cannot change a positive power exponent. The character-existence and character-growth assumptions remain explicit in the final implications.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_nat_sub_one_le_lt {x : ℝ} (hx : 0 < x) : ∃ (k : ℕ), x - 1 ≤ ↑k ∧ ↑k < x

Rounding strictly down works at integers too: use ceil x - 1.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.rpow_exponent_le_of_nat_sub_one_bound {ν τ : ℝ} (hτ : 0 ≤ τ) (hbound : ∀ (d : ℕ), 2 ≤ d → ↑d ^ ν - 1 ≤ ↑d ^ τ) : ν ≤ τ

An additive loss of one does not affect a comparison to a nonnegative power exponent. No sign assumption on the exponent on the left is needed.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exponent_le_of_integer_rounding {ν τ : ℝ} (hτ : 0 ≤ τ) (hround : ∀ (d : ℕ), 2 ≤ d → ∃ (k : ℕ), ↑d ^ ν - 1 ≤ ↑k ∧ ↑k ≤ ↑d ^ τ) : ν ≤ τ

The integer witnesses in the final rounding argument can vary with d.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exponent_le_of_integer_rounding_of_pos {ν τ : ℝ} (hν : 0 < ν) (hround : ∀ (d : ℕ), 2 ≤ d → ∃ (k : ℕ), ↑d ^ ν - 1 ≤ ↑k ∧ ↑k ≤ ↑d ^ τ) : ν ≤ τ

A positive exponent on the left makes the target exponent nonnegative automatically, so it is an alternative to that hypothesis above.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exponent_le_of_detecting_characters {K : Type} [Field K] {ν τ : ℝ} (hτ : 0 ≤ τ) (detect : ∀ (d : ℕ), 2 ≤ d → ∀ (k : ℕ), ↑k < ↑d ^ ν → ∃ (χ : Character K), ↑k ≤ χ.value (Foundation.Tensor.matMul K d d d)) (bound : ∀ (χ : Character K) (d : ℕ), 2 ≤ d → χ.value (Foundation.Tensor.matMul K d d d) ≤ ↑d ^ τ) : ν ≤ τ

Explicitly conditional passage from detecting characters to the exponent bound. The detecting character is allowed to depend on both d and k.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exponent_le_of_detecting_character_exponents {K : Type} [Field K] {ν τ : ℝ} (hτ : 0 ≤ τ) (exponentSum : Character K → ℝ) (value : ∀ (χ : Character K) (d : ℕ), 2 ≤ d → χ.value (Foundation.Tensor.matMul K d d d) = ↑d ^ exponentSum χ) (upper : ∀ (χ : Character K), exponentSum χ ≤ τ) (detect : ∀ (d : ℕ), 2 ≤ d → ∀ (k : ℕ), ↑k < ↑d ^ ν → ∃ (χ : Character K), ↑k ≤ χ.value (Foundation.Tensor.matMul K d d d)) : ν ≤ τ

The character growth bound can be supplied as a uniform bound on its exponent sum, together with the matrix-value identity.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRankExponent_le_nine_quarters_of_characters {K : Type} [Field K] (detect : ∀ (d : ℕ), 2 ≤ d → ∀ (k : ℕ), ↑k < ↑d ^ exactRankExponent K → ∃ (χ : Character K), ↑k ≤ χ.value (Foundation.Tensor.matMul K d d d)) (bound : ∀ (χ : Character K) (d : ℕ), 2 ≤ d → χ.value (Foundation.Tensor.matMul K d d d) ≤ ↑d ^ (9 / 4)) : exactRankExponent K ≤ 9 / 4

The paper's final ν ≤ 9/4 implication, with its two substantive character inputs visible rather than incorporated into the definition of ν.