Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Boundary unit factor: owner 3 cell certificate

Proved
mme_released_boundary_unit_factor_owner3_cell_certificate

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

matrix-multiplication

This is the per-cell part of the numerical certificate for the unit-scale boundary dimension factor of the released global candidate, for owner o=3o=3o=3.

Fix the owner o=3o=3o=3. For a level-3 shape s=(s0,s1,s2)s=(s_0,s_1,s_2)s=(s0​,s1​,s2​) (one of the 454545 triples of naturals with s0+s1+s2=8s_0+s_1+s_2=8s0​+s1​+s2​=8) and a mode m∈{0,1,2}m\in\{0,1,2\}m∈{0,1,2}, let hs,m(w)=wordCounts(o,m,s,w)h_{s,m}(w)=\mathrm{wordCounts}(o,m,s,w)hs,m​(w)=wordCounts(o,m,s,w) be the released unit-scale histogram of the joint rows of the cell sss in mode mmm, over the 818181 words w∈{0,1,2}4w\in\{0,1,2\}^4w∈{0,1,2}4; it equals αo,s\alpha_{o,s}αo,s​ times an integer histogram of total mass 104810^{48}1048, where αo,s\alpha_{o,s}αo,s​ is the released global weight of the cell. Put N=∑whs,m(w)N=\sum_w h_{s,m}(w)N=∑w​hs,m​(w), let ones(w)\mathrm{ones}(w)ones(w) be the number of letters of www equal to 111, and write

H(h)  =  Nlog⁡N−∑wh(w)log⁡h(w)\mathcal H(h)\;=\;N\log N-\sum_w h(w)\log h(w)H(h)=NlogN−w∑​h(w)logh(w)

for the mass entropy (with 0log⁡0=00\log 0=00log0=0). Let πo\pi_oπo​ be the owner's hash orientation (hashMode o).

Claim. For every shape index sss and every mode jjj such that the coordinate πo(j)\pi_o(j)πo​(j) of sss is zero, with m=πo(j+1)m=\pi_o(j+1)m=πo​(j+1),

go,s  ≤  H(hs,m)  +  log⁡5∑whs,m(w) ones(w)  −  81log⁡(6(N+1)),g_{o,s}\;\le\;\mathcal H(h_{s,m})\;+\;\log 5\sum_w h_{s,m}(w)\,\mathrm{ones}(w)\;-\;81\log\bigl(6(N+1)\bigr),go,s​≤H(hs,m​)+log5w∑​hs,m​(w)ones(w)−81log(6(N+1)),

where go,sg_{o,s}go,s​ is the explicit integer listed in the formal statement (entry sss of the list; entries of shapes without a zero coordinate are 000 and unused).

Numerical evidence. The integers go,sg_{o,s}go,s​ were obtained from rigorous rational upper bounds for log⁡(h(w)/N)\log(h(w)/N)log(h(w)/N) (the series log⁡x=2 artanhx−1x+1\log x=2\,\mathrm{artanh}\frac{x-1}{x+1}logx=2artanhx+1x−1​ with 141414 terms after scaling by a power of 222, rounded outward at 10−2010^{-20}10−20), the rational bound log⁡5≥1.6094379124340…\log 5\ge 1.6094379124340\ldotslog5≥1.6094379124340…, and the crude bound 81log⁡(6(N+1))≤81⋅60log⁡10≤1134081\log(6(N+1))\le 81\cdot 60\log 10\le 1134081log(6(N+1))≤81⋅60log10≤11340. Recomputing the right side with 80-digit arithmetic, every cell exceeds its go,sg_{o,s}go,s​, the smallest excess (over all owners) being about 1.29⋅1031.29\cdot10^{3}1.29⋅103. The corner cells s∈{(0,0,8),(0,8,0),(8,0,0)}s\in\{(0,0,8),(0,8,0),(8,0,0)\}s∈{(0,0,8),(0,8,0),(8,0,0)} carry a point-mass histogram and get g=−11340g=-11340g=−11340.

Role. Summing these six owner certificates over the 144144144 boundary cells gives ∑go,s=6⋅1060⋅0.450512205+4.94⋅1051\sum g_{o,s}=6\cdot10^{60}\cdot0.450512205+4.94\cdot10^{51}∑go,s​=6⋅1060⋅0.450512205+4.94⋅1051, which proves the refentropy certificate for the boundary unit factor.

Formalization Note. The histogram is wordCounts o (hashMode o (j + 1)) (shape s) w, which is exactly zCountAt 1 c w for the boundary cell c=(o,shape s)c=(o,\mathrm{shape}\,s)c=(o,shapes) when jjj is its chosen zero mode; for shapes with two zero coordinates every choice gives a point mass. H\mathcal HH is MME.RegionRate.massEntropy. The bound go,sg_{o,s}go,s​ is written as (L : List ℤ).getD s.val 0.

Preamble
import Definitions.Def_mme_released_global_two_part_split_data
import Definitions.Def_mme_graded_integer_regional_step_data
import Definitions.Def_mme_regional_entropy_rate_data
open BigOperators MME MME.ProfiledCW MME.GlobalCW MME.RecursiveYZ MME.CompleteSplit
  MME.ReleasedGlobal MME.RegionRealization MME.ReleasedRecursive.Asm
open scoped Classical
set_option autoImplicit false
Formal statement
theorem mme_released_boundary_unit_factor_owner3_cell_certificate :
    ∀ s : Fin 45, ∀ j : Fin 3, ((shape s).val (hashMode 3 j)).val = 0 →
      (((([-11340, 49668638953335937711494407889999999999999999999999988660, 2487054614052835827274540989923914242287599999999999988660, 30163457323921081036836740497777357908594479999999999988660, 85576822698613846420966205898577990636333499999999999988660, 30067821815260713614855217735416686177409899999999999988660, 2517127730131430968763365329694453098933599999999999988660, 49831181395034422796165836269999999999999999999999988660, -11340, 49330957015728673580320238579999999999999999999999988660, 0, 0, 0, 0, 0, 0, 49418204722463656064119322219999999999999999999999988660, 2462068005478363244010228809702955347881919999999999988660, 0, 0, 0, 0, 0, 2503068561839493136596560736699408200679719999999999988660, 29847084297034320675171170643286993871946239999999999988660, 0, 0, 0, 0, 29843979565434056677502802586522355812502399999999999988660, 85531596254473738478550523165445700391203929999999999988660, 0, 0, 0, 83903297232204125136362308689246215693550539999999999988660, 30295951027595430271979843192587435907283139999999999988660, 0, 0, 29916676812800300703822801098051560520921769999999999988660, 2563402632647972734417760073255230423555679999999999988660, 0, 2532342617935787971070182359696690820563059999999999988660, 49928473792082631357020898739999999999999999999999988660, 49653342744347171725974626229999999999999999999999988660, -11340] : List ℤ).getD s.val 0 : ℤ)) : ℝ) ≤
        MME.RegionRate.massEntropy
            (fun w => (wordCounts 3 (hashMode 3 (j + 1)) (shape s) w : ℝ)) +
          ((∑ w, wordCounts 3 (hashMode 3 (j + 1)) (shape s) w * Boundary.ones w : ℕ) : ℝ) *
            Real.log 5 -
          81 * Real.log (6 * (((∑ w, wordCounts 3 (hashMode 3 (j + 1)) (shape s) w : ℕ) : ℝ) + 1)) := by sorry
Source
Prove2Me mission 7e65274f (More Asymmetry Bound: omega < 2.37134), WP7 boundary part of the dimension certificate; released data of Alman-Duan-Vassilevska Williams-Xu-Xu-Zhou, arXiv 2404.16349v3; per-owner split of mme_released_boundary_unit_factor_mass_entropy_certificate (559ea2ba).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me