Fine-coordinate count of the replicated released profile

Proved

mme_released_116_scaled_fine_coordinate_card

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

regional-extractiontensor-complexity

The two child positions of every parent occurrence, each carrying a length-two complete word, give exactly four times k times the fourth power of the seed denominator fine coordinates.

Preamble

import Theorems.Thm_mme_released_116_regional_total
import Definitions.Def_mme_released_116_integer_profiles
import Mathlib.Data.Fintype.Sigma
import Mathlib.Analysis.SpecialFunctions.Log.Base
import Mathlib.Algebra.Order.Archimedean.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
import Definitions.Def_mme_recursive_yz_CW_cells
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Tactic.Positivity
open BigOperators MME MME.RecursiveYZ MME.RecursiveYZ.CWCells MME.CompleteSplit
open scoped Classical
open MME.Released116 MME.MoreAsymmetryExactSeed
set_option autoImplicit false
universe u

Formal statement

theorem mme_released_116_scaled_fine_coordinate_card (k : ℕ) :
    Fintype.card (Position (fun r : Fin 6 => k * regionalSize r)) * 2 ^ (2 - 1) =
      4 * (k * denominator ^ 4) := by sorry

Source

Selected-count logarithms and uniformly controlled repair for the concrete released regional extraction.

View graph