Physical child coordinates agree with literal parent-word splitting

Proved

mme_regional_parent_partition_fine_coordinates

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

regional-extractiontensor-complexity

Suppose $T$ parent positions are partitioned into regions of sizes $n_r$ . There exists an ordering of the $2T$ child positions such that, for every fine word of length $4T$ , grouping its letters into length-two child words in that order agrees with grouping into length-four parent words and taking the literal left and right halves. The equality holds at every region, parent position and child side. This identifies the physical coordinate ordering used by extraction with the ordering in the released histogram windows.

Preamble

import Definitions.Def_mme_recursive_profiled_CW_data
import Definitions.Def_mme_complete_split_concatenation
import Mathlib.Logic.Equiv.Prod
import Mathlib.Tactic.FinCases

open BigOperators MME MME.RecursiveYZ MME.CompleteSplit
set_option autoImplicit false

Formal statement

theorem mme_regional_parent_partition_fine_coordinates
    {R T : ℕ} {n : Fin R → ℕ}
    (positions : (Σ r, Fin (n r)) ≃ Fin T) :
    ∃ childPositions : Fin (T * 2) ≃ Position n,
      ∀ (x : ProfiledCW.FineWord (T * 4)) (p : Position n),
        ProfiledCW.split childPositions (show (T * 2) * 2 ^ (2 - 1) = T * 4 by omega) x p =
          (let v := completeWordSplitEquiv 2 (by decide)
            (ProfiledCW.split (Equiv.refl (Fin T)) rfl x (positions ⟨p.1,p.2.1⟩))
          ![v.1,v.2] p.2.2) := by sorry

Source

Physical regional partitions and literal complete-word concatenation.

View graph