Mass-entropy certificate for the zero level-2 halves

Proved

mme_released_level2_zero_half_mass_entropy_certificate

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

matrix-multiplication

This is the numeric entropy certificate for the zero level-2 halves of the released recursion (WP6/WP7, zero-half boundary). It is a single fixed inequality between real numbers.

Setting. Let $D=10^{12}$ . A zero cell is a pair $z=(\rho,c)$ where $\rho\in\mathrm{Fin}\,6$ is a level-3 region and $c=(r,s)\in\mathrm{Cell}(4,88,\texttt{parent3}\,\rho)$ is a level-3 cell whose half-grade triple $s$ has a zero coordinate. Let $j_0(z)$ be the first zero coordinate of $s$ , and let $j(z)=j_0(z)+1\in\mathbb Z/3$ be the next mode. Let $\mu_z(w)=\mu^{(3)}_\rho(j(z),c,w)$ (RecStage.mu3) for the nine complete level-2 words $w$ , and let $\mathrm{ones}(w)$ count the letters of $w$ equal to $1$ . For masses $x:W\to\mathbb R_{\ge0}$ with total $X$ , the mass entropy is

H(x)=X\log X-\sum_w x_w\log x_w .

Claim.

12546098100\cdot10^{51}\ \le\ \sum_{z}\Big(H(\mu_z)+\Big(\sum_w\mu_z(w)\,\mathrm{ones}(w)\Big)\log5\Big),

where the sum runs over all zero cells.

Why it should hold. The right side is the unit-scale logarithm (before the multinomial loss) of the refzero-half boundary dimension product. It is mode-independent: the zero mode has a single word, and the two other modes are exchanged by flipLabel. Evaluated exactly from the released tables with 80-digit logarithms, it equals $1.25460982350006\cdot10^{61}=2.09101637250\ldots\cdot6D^5$ . That is $1.35\cdot10^{52}$ (relative $1.1\cdot10^{-9}$ ) above the claimed bound. There are $2604$ zero cells, $434$ per region. Every cell's word distribution is $\mu_z(w)=M(z)\,d_z(w)/D$ with $\sum_w d_z(w)=D$ , where $M(z)$ is the cell mass.

The certificate splits into six regional certificates, one per $\rho$ .

Preamble

import Definitions.Def_mme_released_recursive_stage_data
import Definitions.Def_mme_graded_integer_regional_step_data
import Definitions.Def_mme_regional_entropy_rate_data
open BigOperators MME MME.RecursiveYZ
set_option autoImplicit false

Formal statement

theorem mme_released_level2_zero_half_mass_entropy_certificate :
    ((12546098100 * 10 ^ 51 : ℕ) : ℝ) ≤
      ∑ z : (ρ : Fin 6) × {c : Cell (2 * 2 ^ (2 - 1)) 88 (RecStage.parent3 ρ) //
          ∃ j, (c.2.val j).val = 0},
        (MME.RegionRate.massEntropy (fun w ↦ (RecStage.mu3 z.1
            (if (z.2.1.2.val 0).val = 0 then 1 else if (z.2.1.2.val 1).val = 0 then 2 else 0)
            z.2.1 w : ℝ)) +
          ((∑ w, RecStage.mu3 z.1
            (if (z.2.1.2.val 0).val = 0 then 1 else if (z.2.1.2.val 1).val = 0 then 2 else 0)
            z.2.1 w * Boundary.ones w : ℕ) : ℝ) * Real.log 5) := by
  sorry

Source

Prove2Me mission 7e65274f (More Asymmetry Bound: omega < 2.37134); WP6/WP7 of marwahaha's plan comment of 2026-09-24; released data of Alman-Duan-Vassilevska Williams-Xu-Xu-Zhou, More Asymmetry Yields Faster Matrix Multiplication, arXiv 2404.16349. Entropy value computed from the released tables (RecStage.mu3).

View graph