Certified numerical extraction of the physical six-region interface

Proved

mme_released_global_six_region_numerical_extraction

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

matrix-multiplicationmore-asymmetrytensor-restriction

Set $G=2235998128/1500000000$ , $B=D^5k^2$ , and $n=6B$ . Over any field and for any six positive tolerance caps, choose fixed positive regional tolerances below those caps. At every sufficiently large integer square scale, there are physical Parts on all six regions, a joint interface $Q$ , and positive input and output counts $U,V$ with

1\leq U\leq(B+1)^{65610},\qquad e^{nG}U\leq V,\qquad \bigoplus_V T(Q)\ \preceq\ \bigoplus_U\mathrm{CW}_5^{\otimes 4n}.

The conclusion also retains each Part and its separate numerical bound for later assembly. This is an unconditional numerical global extraction for the exact published candidate; no recursive copy or matrix-dimension claim is assumed or concluded.

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_six_region_numerical_extraction {K : Type u} [Field K] (eta : Fin 6 → ℝ) (heta : ∀ 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),
      ∃ S : ∀ o, Part (4 * blocks (k^2)) 3 (physicalWindow o (k^2) hk (a o) (eps o)),
        (∀ o, 1 ≤ (S o).inputs ∧ (S o).inputs ≤ (blocks (k^2)+1)^10935 ∧
          usableRate o * (blocks (k^2) : ℝ) + Real.log ((S o).inputs : ℝ) ≤ (S o).rate) ∧
        1 ≤ (∏ o, (S o).inputs) ∧ (∏ o, (S o).inputs) ≤ (blocks (k^2)+1)^65610 ∧
        ∃ outputs : ℕ,
          Real.exp ((6 * blocks (k^2) : ℕ) * ((2235998128 : ℝ)/1500000000)) *
            ((∏ o, (S o).inputs : ℕ) : ℝ) ≤ (outputs : ℝ) ∧
          Restrict (bigAdd (fun _ : Fin outputs ↦ tensor K (jointWindow (k^2) hk a eps)))
            (bigAdd (fun _ : Fin (∏ o, (S o).inputs) ↦
              (CWObj K 5).kronPow (4 * (6 * blocks (k^2))))) := 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