Large-N surplus recipe exists

Open

mme_entropy_regional_largeN_surplus_witness

by Tamas Fulop · Sep 19, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

matrix-multiplicationmore-asymmetryregional-entropy

There is a large-level entropy recipe witnessing surplus.

Let $N$ , $\ell$ , $P$ , and $D$ range over levels, sizes, profile predicates, and finite entropy recipes in the More Asymmetry regional setting. Write $I(D)$ for charged inputs, $O(D)$ for guaranteed outputs, and $a(D),b(D),c(D)$ for matrix dimensions. Let $\tau=3952233/5000000$ .

I(D)\cdot 7^N < O(D)\cdot [a(D)b(D)c(D)]^{\tau}.

Then there exist $N$ , $\ell$ , $P$ , and $D$ with $N\ge 3$ , $I(D)=1$ , $a(D)b(D)c(D)\ge 1$ , and the displayed strict surplus inequality. This is the remaining large-level existence obligation after small levels are ruled out: small- $N$ recipes never satisfy surplus, so any witness must come from $N\ge 3$ with genuine entropy copies and matching boundary data from the Section 6 numerical solution.

Formalization Note Lean states existence with explicit level, size, and predicate binders over EntropyRecipe.

Preamble

import Definitions.Def_mme_entropy_regional_CW_recipe
open MME MME.ProfiledCW MME.RegionRealization
set_option autoImplicit false

Formal statement

theorem mme_entropy_regional_largeN_surplus_witness : exists (N ell : Nat) (P : MME.ProfiledCW.Predicate N) (D : EntropyRecipe N ell P), 3 <= N /\ D.inputs = 1 /\ 1 <= D.a * D.b * D.c /\ (((D.inputs * 7 ^ N : Nat) : Real) < (D.outputs : Real) * (((D.a * D.b * D.c : Nat) : Real) ^ ((3952233 : Real) / 5000000))) := by sorry

Source

Uniform entropy-based integer regional construction for the More Asymmetry matrix multiplication campaign, https://arxiv.org/html/2404.16349v2#S6 . Large-N existence obligation after small-N delimitation; Section 6 numerical solution and Table 1.

View graph