owner0 mode2 compatibility interior mass row4

Disproved

mme_released_global_owner0_mode2_compatibility_interior_mass_row4

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

exact-arithmeticmatrix-multiplication

This unproved helper was generated with an incorrect boundary predicate: mode 2 requires coordinate 0 = 0 OR coordinate 1 = 0. It is superseded by mme_released_global_owner0_mode2_compatibility_yz_interior_mass_row4. No proof of this incorrect statement was submitted. The original compatibility entropy theorem is unchanged.

Preamble

import Definitions.Def_mme_released_global_profile_data
open scoped BigOperators
open MME MME.ReleasedGlobal MME.MoreAsymmetryExactSeed

Formal statement

theorem mme_released_global_owner0_mode2_compatibility_interior_mass_row4 : ∀ w : Word,
    ((([0, 0, 0, 0, 0, 0, 0, 0, 53441581206410233573904040111711000000000000000000000000, 0, 0, 0, 0, 0, 2965123937020559558017583576178697750000000000000000000000, 0, 2965123937020559558017583576178697750000000000000000000000, 0, 0, 0, 59471268191501827778707768870591792348262372625704017995, 0, 2903627278750932927024745421207394389119178184748591964010, 0, 59471268191501827778707768870591792348262372625704017995, 0, 0, 0, 0, 0, 0, 0, 2965123937020559558017583576178697750000000000000000000000, 0, 2965123937020559558017583576178697750000000000000000000000, 0, 0, 0, 2903627368168540781952915533078827705381348706748591964010, 0, 129226369078973424338427304220106615641605896726502816071980, 0, 2903627368168540781952915533078827705381348706748591964010, 0, 0, 0, 2965123796925380060722915029694160500000000000000000000000, 0, 2965123796925380060722915029694160500000000000000000000000, 0, 0, 0, 0, 0, 0, 0, 59471268191501827778707768870591792348262372625704017995, 0, 2903627278750932927024745421207394389119178184748591964010, 0, 59471268191501827778707768870591792348262372625704017995, 0, 0, 0, 2965123796925380060722915029694160500000000000000000000000, 0, 2965123796925380060722915029694160500000000000000000000000, 0, 0, 0, 0, 0, 53441129431452223966644332235429000000000000000000000000, 0, 0, 0, 0, 0, 0, 0, 0] : List ℕ).getD (27 * (w 0).val + 9 * (w 1).val + 3 * (w 2).val + (w 3).val) 0 : ℕ) : ℚ) / 1000000000000000000000000000000000000000000000000000000000000 =
    ∑ s : Fin 45, if ¬ ((shape s).val 1).val = 0 ∧ (shape s).val 2 = 4 then ((alpha 0 s * ((jointRows 0 s).map (fun a => if atom a.1 2 = w then a.2 else 0)).sum : ℕ) : ℚ) / (denominator : ℚ) ^ 5 else 0 := by sorry

Source

Exact released rational CW profile and joint atom counts.

View graph