Replication preserves the released extraction divisor and size lower bound

Proved

mme_released_116_scaled_integer_divisibility

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

regional-extractiontensor-complexity

For every positive integer $k$ , the released owner-zero $(1,1,6)$ data satisfy

0<kd^2,\qquad kd^2\le kn_r,\qquad kd^2\mid km_r(c)

for all regions and admissible splits, with $d=10^{12}$ . The common extraction minimum therefore grows linearly with replication.

Preamble

import Definitions.Def_mme_released_116_integer_profiles
import Mathlib.Algebra.Order.Archimedean.Basic
import Mathlib.Tactic.NormNum

open BigOperators MME MME.Released116 MME.MoreAsymmetryExactSeed
set_option autoImplicit false

Formal statement

theorem mme_released_116_scaled_integer_divisibility (k : ℕ) (hk : 0 < k) :
    0 < k * denominator ^ 2 ∧
      (∀ r : Fin 6, k * denominator ^ 2 ≤ k * regionalSize r) ∧
      ∀ (r : Fin 6) (c : Split), k * denominator ^ 2 ∣ k * splitCount r c := by sorry

Source

Integer replication of regional profiles and the released owner-zero (1,1,6) component.

View graph