Integer entropy step with at least five guaranteed copies

Disproved

mme_entropy_regional_step_five_copies

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

matrix-multiplicationmore-asymmetryregional-entropy

Fix $N=2$ in the More Asymmetry regional setting. There is a finite integer entropy step $S$ at some level $lower$ , over the trivially true predicate, whose guaranteed entropy copy count is at least five. In particular

5 \le S.entropyCopies.

This child isolates the analytic core of the witness: with the trivial predicate the admissibility side conditions hold by truth, so only the quantitative copy bound must be constructed. The regional entropy rate, with all finite polynomial, AP-free-set, floor and repair losses included, must clear five copies after division by the repair power.

Formalization Note Lean states the step with existential level and a fixed trivial predicate on $N=2$ .

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_step_five_copies : ∃ (lower : ℕ) (S : IntegerStep lower 2 (fun _ _ ↦ True)), 5 ≤ S.entropyCopies := by sorry

Source

Uniform entropy-based integer regional construction for the More Asymmetry matrix multiplication campaign, https://arxiv.org/html/2404.16349v2#S6 . This child isolates the quantitative five-copy integer step; the matching boundary data is a separate child.

View graph