Zero-half mass-entropy certificate, region 4

Proved

mme_released_level2_zero_half_region4_mass_entropy_certificate

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

matrix-multiplication

This is the region- $4$ part of the refzero-half mass-entropy certificate of the released recursion. It is a single fixed numerical inequality.

Setting. Let $D=10^{12}$ and $\rho=4$ . A zero cell of region $\rho$ is a level-3 cell $c=(r,s)\in\mathrm{Cell}(4,88,\texttt{parent3}\,\rho)$ whose half-grade triple $s$ has a zero coordinate. Let $j(c)=j_0(c)+1$ , where $j_0(c)$ is the first zero coordinate of $s$ . Let $\mu_c(w)=\mu^{(3)}_\rho(j(c),c,w)$ (RecStage.mu3) for the nine complete level-2 words $w$ , and let $\mathrm{ones}(w)$ be the number of letters of $w$ equal to $1$ . The mass entropy of masses $x$ with total $X$ is $H(x)=X\log X-\sum_w x_w\log x_w$ .

Claim.

T_{4}\ \le\ \sum_{c}\Big(H(\mu_c)+\Big(\sum_w\mu_c(w)\,\mathrm{ones}(w)\Big)\log5\Big),\qquad T_{4}=2101764658211037000000000000000000000000000000000000000000000,

where the sum runs over the zero cells of region $4$ .

Why it should hold. There are $434$ zero cells. For each one, $\mu_c=M(c)\,d_c/D$ , where $M(c)$ is the cell mass (a multiple of $D$ ) and $d_c$ is the list of childW weights, which sums to $D$ . So $H(\mu_c)=M(c)\,h(d_c/D)$ , where $h$ is the Shannon entropy.

Each $\log(d/D)$ is bounded above by the certified rational series of refthe rational log series certificate, with $14$ terms and a dyadic shift.
The refrational entropy bounds turn these into a rational lower bound for $h$ .
$\log5$ is bounded below by the same series.

The resulting exact rational lower bound for the sum exceeds $T_{4}$ . The true value (80-digit logarithms) is larger than $T_{4}$ by a relative margin of $1.0\cdot10^{-10}$ .

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_region4_mass_entropy_certificate :
    ((2101764658211037000000000000000000000000000000000000000000000 : ℕ) : ℝ) ≤
      ∑ c : {c : Cell (2 * 2 ^ (2 - 1)) 88 (RecStage.parent3 4) // ∃ j, (c.2.val j).val = 0},
        (MME.RegionRate.massEntropy (fun w ↦ (RecStage.mu3 4
            (if (c.1.2.val 0).val = 0 then 1 else if (c.1.2.val 1).val = 0 then 2 else 0)
            c.1 w : ℝ)) +
          ((∑ w, RecStage.mu3 4
            (if (c.1.2.val 0).val = 0 then 1 else if (c.1.2.val 1).val = 0 then 2 else 0)
            c.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