Complex arithmetic programs and asymptotic matrix multiplication costs.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.eval_eq_constant_or_input_of_cost_eq_zero {Input : Type u_1} {r : ℕ} (p : Program Input r) (hp : p.cost = 0) (i : Fin r) : (∃ (z : ℂ), ∀ (inputs : Input → ℂ), p.eval inputs i = z) ∨ ∃ (a : Input), ∀ (inputs : Input → ℂ), p.eval inputs i = inputs a

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.one_le_cost {n : ℕ} (P : MatrixAlgorithm n) (hn : 1 ≤ n) (hP : P.Correct) : 1 ≤ P.cost

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_nonneg {τ : ℝ} (hτ : AdmissibleExponent τ) : 0 ≤ τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_bddBelow : BddBelow {τ : ℝ | AdmissibleExponent τ}