Normalize the exact recursive parent mixture

Proved

mme_released_recursive_profile_normalization

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

exact-profilematrix-multiplicationmore-asymmetry

Let $D=10^{12}$ . For every primitive seed term $t$ , physical mode $i$ , and four-letter word $w$ , its integer parent marginal $C_t(i,w)$ satisfies

\frac{C_t(i,w)}{D^4}=P_t(i,w).

For an interior term, $P_t$ is the sum over six recursive regions of the region weight times the split-weighted product of the left and right child square-word marginals. For a boundary term, $P_t$ is its explicit terminal marginal. This identity relates integer counts to normalized frequencies without approximation.

Preamble

import Definitions.Def_mme_released_recursive_profile_mixture
open BigOperators MME MME.ReleasedGlobal MME.ReleasedMixture
set_option autoImplicit false

Formal statement

theorem mme_released_recursive_profile_normalization (t : SeedTerm) (i : Fin 3) (w : Word) :
    (parentCount t i w : ℝ) / (D : ℝ)^4 = parentProfile t i w := by sorry

Source

Exact-seed profile bridge for the six-region global interface in More Asymmetry Yields Faster Matrix Multiplication, https://arxiv.org/html/2404.16349v2. Uses the already published primitive rational seed and literal supported joint counts; the recursive numerical continuation remains a separate obligation.

View graph