ω(F) ≤ 9/4 over every field

The auxiliary-separation argument is carried out over an arbitrary algebraically closed field K (AuxiliarySeparation.omega_le_nine_quarters; the only characteristic-dependent step, the Fourier separation, uses a period L ∈ {3M - 2, 3M - 1} that is nonzero in K instead of the paper's 5M).

For an arbitrary field F let P be its prime field (ℚ or ZMod p) and K = AlgebraicClosure P. A near-optimal decomposition of ⟨u,u,u⟩ over K has its coefficients in a finite extension E / P of some degree m; tensor powering over E and descending to P gives decompositions of ⟨uʲ,uʲ,uʲ⟩ over P of size m³ rʲ, which map into F. The constant m³ is absorbed by taking j large. The field-generic block recursion then gives the arithmetic bound over F.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AllFields.omega_le_nine_quarters_of_ringHom (P : Type) [Field P] {F : Type u_1} [Field F] (f : P →+* F) : Arithmetic.omega F ≤ 9 / 4

If F receives a ring homomorphism from a field P, then ω(F) ≤ 9/4.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.omega_le_nine_quarters_all_fields (F : Type u_1) [Field F] : Arithmetic.omega F ≤ 9 / 4

The matrix multiplication exponent is at most 9/4 over every field.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.admissibleExponent_nine_quarters_all_fields (F : Type u_1) [Field F] : Arithmetic.AdmissibleExponent F (9 / 4)

Non-vacuity: over every field the exponent 9/4 is itself admissible, i.e. for every ε > 0 one constant C bounds the cost of correct division-free programs for n × n matrix multiplication by C n^(9/4 + ε) at every size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.matrix_multiplication_cost_le_all_fields (F : Type u_1) [Field F] (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∃ (P : Arithmetic.MatrixAlgorithm F n n n), P.Correct ∧ ↑P.cost ≤ C * ↑n ^ (9 / 4 + ε)

The unfolded form of the all-fields statement.