Recursive continuation of the concrete six-region global interface

Open

mme_released_global_joint_recursive_continuation

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

matrix-multiplicationmore-asymmetrytensor-restriction

This is the remaining recursive certificate for the published exact global candidate. Set $B=D^5k^2$ and $n=6B$ . Prove that there are six positive tolerance caps such that, for every choice of smaller positive regional tolerances and every lower bound on $k$ , some larger integer $k$ has the following property: for every admissible reference arrangement of the six global profiles, their concrete physical joint window admits one logarithmic joint recipe $R$ at level three, with input count $U_R\geq1$ , positive dimension product $abc$ , and

n\frac{1322355}{1000000}+\log U_R\leq L_R,

n\left(3\frac{209612367517}{100000000000}-10^{-7}\right)\leq\log(abc).

The tolerance caps must be chosen before the common scale. The recipe acts on the entire global interface, allowing joint regional stages. This statement does not assume a tensor restriction or the missing numerical budgets: constructing the recipe and proving both budgets is the obligation. Existing external interval calculations motivate the strict recursive rate, but are not a Lean proof of this statement.

Preamble

import Definitions.Def_mme_released_global_joint_interface
open BigOperators MME MME.TensorObj MME.ProfiledCW MME.GlobalCW MME.RegionRealization MME.ReleasedGlobal
set_option autoImplicit false
universe u

Formal statement

theorem mme_released_global_joint_recursive_continuation :
    ∃ eta : Fin 6 → ℝ, (∀ o, 0 < eta o) ∧
      ∀ eps : Fin 6 → ℝ, (∀ o, 0 < eps o) → (∀ o, eps o ≤ eta o) →
        ∀ k0 : ℕ, ∃ k : ℕ, k0 ≤ k ∧
          ∀ (hk : 0 < k^2) (a : ∀ o : Fin 6, Reference o (k^2)),
            ∃ R : LogJointRecipe (4 * (6 * blocks (k^2))) 3 (jointWindow (k^2) hk a eps),
              1 ≤ R.inputs ∧ 1 ≤ R.a * R.b * R.c ∧
              (6 * blocks (k^2) : ℕ) * ((1322355 : ℝ)/1000000) +
                Real.log (R.inputs : ℝ) ≤ R.logOutputs ∧
              (6 * blocks (k^2) : ℕ) *
                (3 * ((209612367517 : ℝ)/100000000000) - 1/10000000) ≤
                  Real.log ((R.a * R.b * R.c : ℕ) : ℝ) := by sorry

Source

Auxiliary formalization for Alman et al., More Asymmetry Yields Faster Matrix Multiplication, https://arxiv.org/html/2404.16349v2, Theorem 5.3, Section 5.1, Theorem 6.4 and Algorithm 1. Specialization to the published exact ReleasedGlobal seed; the numerical recursive continuation remains an explicit separate obligation.

View graph