Core graded recursive construction for the released global candidate

Proved

mme_released_global_graded_joint_recursive_construction

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

matrix-multiplicationmore-asymmetryrecursive

Construct the graded-source logarithmic joint recipe required by the released global candidate. This is the core recursive continuation obligation: it supplies positive tolerance caps, a common sufficiently large scale, a graded joint recipe for every admissible reference arrangement, and the two explicit logarithmic budget inequalities. It is the construction layer used by the parent continuation theorem.

Preamble

import Definitions.Def_mme_released_global_joint_interface
import Definitions.Def_mme_graded_integer_regional_step_data
open BigOperators MME MME.ProfiledCW MME.GlobalCW MME.RegionRealization MME.ReleasedGlobal
set_option autoImplicit false

Formal statement

theorem mme_released_global_graded_joint_recursive_construction :
    ∃ 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 : LogJointRecipeG (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) : ℝ) * ((13223546 : ℝ)/10000000) +
                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

Alman-Duan-Vassilevska Williams-Xu-Xu-Zhou, https://arxiv.org/abs/2404.16349, Sections 5-6

View graph