Nonempty graded tolerance stages for all released positive frames at square scales

Proved

mme_released_square_scale_graded_tolerance_stages

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

entropyformalizationmatrix-multiplicationregional-extraction

For each of the six released inner regions $\rho$ , choose a nonnegative requested rate $r_\rho$ strictly below its canonical central regional entropy rate. Given any positive parent-tolerance cap, there are a common child-band radius $\delta>0$ , with $4\delta\le\mathrm{cap}$ , and a common scale threshold with the following property.

For every sufficiently large natural number $k$ and every positive integer frame at scale $k^2$ in any region, set

\varepsilon_k=\sqrt{\frac{A(k+2)}{D^2k^2}},\qquad A=8\cdot25\cdot88\cdot9^2,\qquad D=10^{12}.

Then $k>1$ , $\varepsilon_k>0$ , $\varepsilon_k+2\delta\le\mathrm{cap}$ , and the exact size test holds with minimum $k^2D^2$ and repair base $k$ . The transparent frame constructor gives a central step with its original counts, positions, and reference address. There exists a graded extraction stage from the common-coordinate parent-graded band of radius cap to the whole child window of radius $\delta$ around that central step. Its logarithmic rate is exactly $r_\rho k^2$ , and its number of cases is at most

\bigl(2\operatorname{blocks}(\rho,k^2)+1\bigr)^{27C_\rho},\qquad C_\rho=|\operatorname{Cell}(4,88,\operatorname{parent3}(\rho))|.

The scale threshold precedes quantification over the region, frame, reference, and varying child profiles. Every supported triple in the target window belongs to exactly one case. A supported triple with the exact central child histograms exists for the same frame, so the number of cases is at least one. The strict central-rate margins remain explicit hypotheses. The uniform varying-profile budget, central supported witness, and extraction stage follow from accepted interfaces. Numerical rate certification and the recursive continuation are separate obligations.

Preamble

import Definitions.Def_mme_released_positive_integer_frame_data
import Definitions.Def_mme_regional_tolerance_window_data

open BigOperators Filter MME MME.ProfiledCW MME.RecursiveYZ MME.RegionRealization
  MME.CompleteSplit MME.MoreAsymmetryExactSeed MME.ReleasedPositiveInteger
set_option autoImplicit false

Formal statement

theorem mme_released_square_scale_graded_tolerance_stages
    (rates : Fin 6 → ℝ) (rates_nonneg : ∀ region, 0 ≤ rates region)
    (rates_below : ∀ region, rates region < RegionRate.regionalRate
      (RecStage.htotal3 region) (RecStage.n3 region)
      (RecStage.m3 region) (RecStage.mu3 region))
    (cap : ℝ) (cap_pos : 0 < cap) :
    ∃ delta : ℝ, 0 < delta ∧ 4 * delta ≤ cap ∧
      ∀ᶠ k : ℕ in atTop,
        ∃ repair_gt_one : 1 < k,
        ∃ epsilon_pos : 0 < (Real.sqrt ((8 * 25 * 88 * (Fintype.card (CompleteWord 2) : ℝ) ^ 2 / (denominator : ℝ) ^ 2) * ((k + 2 : ℕ) : ℝ) / (k : ℝ) ^ 2)),
        ∃ size_test : (8 * k : ℝ) *
          (25 * 88 * (Fintype.card (CompleteWord 2) : ℝ) ^ 2) ≤
            ((k ^ 2 * denominator ^ 2 : ℕ) : ℝ) * ((Real.sqrt ((8 * 25 * 88 * (Fintype.card (CompleteWord 2) : ℝ) ^ 2 / (denominator : ℝ) ^ 2) * ((k + 2 : ℕ) : ℝ) / (k : ℝ) ^ 2))) ^ 2,
          (Real.sqrt ((8 * 25 * 88 * (Fintype.card (CompleteWord 2) : ℝ) ^ 2 / (denominator : ℝ) ^ 2) * ((k + 2 : ℕ) : ℝ) / (k : ℝ) ^ 2)) + 2 * delta ≤ cap ∧
          ∀ (region : Fin 6) (frame : Frame region (k ^ 2)),
            ∃ stage : LogPartStageG (ReleasedJointInterior.blocks region (k ^ 2) * 4)
                2 (fun i x => ParentGraded (ReleasedJointInterior.parent region) (ReleasedJointInterior.size region (k ^ 2)) i (split (ell := 2) (ReleasedJointInterior.positions region (k ^ 2)) (ReleasedJointInterior.positions_length region (k ^ 2)) x) ∧ ReleasedJointInterior.source region (k ^ 2) cap i x) (childWindow (frame.step (pow_pos (lt_trans Nat.zero_lt_one repair_gt_one) 2) k repair_gt_one (Real.sqrt ((8 * 25 * 88 * (Fintype.card (CompleteWord 2) : ℝ) ^ 2 / (denominator : ℝ) ^ 2) * ((k + 2 : ℕ) : ℝ) / (k : ℝ) ^ 2)) epsilon_pos size_test) delta),
              stage.rate = rates region * (k : ℝ) ^ 2 ∧
              stage.types ≤ (2 * ReleasedJointInterior.blocks region (k ^ 2) + 1) ^
                (27 * Fintype.card (Cell 4 88 (RecStage.parent3 region))) ∧
              1 ≤ stage.types := by sorry

Source

Composition of the [positive integer frame](p2m:theorem/8aa8d8f3-b4a4-4716-9fdf-b63581bd2434), [uniform square-scale regional budget](p2m:theorem/2273afa5-2570-43da-8e72-84e0630074d4), [graded tolerance-window construction](p2m:theorem/eb6196aa-a575-44a7-9fed-0707feda27f3), and [supported central child words](p2m:theorem/468b9470-63e3-4063-9982-d6affa3078b3), using the [canonical frame definition](p2m:theorem/c931a3dd-5756-487f-9bc2-693b71748249). The regional budget adapts marwahaha's accepted entropy-continuity proof, and the graded cover adapts raresbuhai's accepted profile enumeration. The underlying extraction method is Alman et al., More Asymmetry Yields Faster Matrix Multiplication, https://arxiv.org/html/2404.16349v2#S6. This is a composition of formal interfaces for the released data, not a verbatim theorem from the paper or a new exponent claim.

View graph