Prove2Me

Explicit polynomial completion ratio for phi_224 profiles

Proved
mme_stothers_phi224_polynomial_completion_ratio

by marwahaha · Sep 5, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

algebraic-complexitycombinatoricsentropylaser-methodmatrix-multiplicationtype-2

Let N>0N>0 and let α+2β+γ+δ=N\alpha+2\beta+\gamma+\delta=N. Write SS for the family of all length-2N2N words in the nine fine φ224\varphi_{224} types with the prescribed three projected marginals, and write S0S_0 for the distinguished exact-profile family with multiplicities

(α,β,γ,β,2δ,β,γ,β,α).(\alpha,\beta,\gamma,\beta,2\delta,\beta,\gamma,\beta,\alpha).

Then

∣S∣≤(2N+1)9(6(2N+1))9∣S0∣.|S|\leq (2N+1)^9\bigl(6(2N+1)\bigr)^9|S_0|.

Thus every same-marginal completion is controlled by the exact symmetric family up to an explicit degree-1818 polynomial factor. This is the finite completion-ratio input used to bound the relative collision degree in the type-2 affine-hashing extraction.

Preamble
import Definitions.Def_mme_stothers_phi224_profile_data
import Theorems.Thm_mme_stothers_phi224_marginal_profile_entropy_upper
import Theorems.Thm_mme_stothers_phi224_exact_profile_entropy_polynomial_lower

set_option autoImplicit false
Formal statement
theorem mme_stothers_phi224_polynomial_completion_ratio
    (N alpha beta gamma delta : ℕ) (hN : 0 < N)
    (hsum : alpha + 2 * beta + gamma + delta = N) :
    (Nat.card
        (MME.StothersFourth.Phi224.MarginalProfileWord
          N alpha beta gamma delta) : ℝ) ≤
      ((((2 * N + 1 : ℕ) : ℝ)) ^ 9 *
        (6 * (((2 * N + 1 : ℕ) : ℝ))) ^ 9) *
        (Nat.card
          (MME.StothersFourth.Phi224.ExactProfileWord
            N alpha beta gamma delta) : ℝ) := by
  sorry
Source
A. M. Davie and A. J. Stothers, Improved Bound for Complexity of Matrix Multiplication (2013), equations (3.5)--(3.6) and Lemma 5.1(iv), pp. 359--360 and 365--366, https://www.maths.ed.ac.uk/~sandy/a11164.pdf.

View graph