The compact released regions admit positive integer frames
Provedmme_released_positive_integer_frameFor every released inner region and every natural-number scale , there exists a positive integer frame for the 88 compact labels of that region.
The frame uses the exact scaled data , , and . It contains a reference address with the prescribed split histogram, enumerations of all parent and child positions, exact marginal masses, grade support, boundary symmetry, minimum parent size , and split-count divisibility by , where . Its child enumeration preserves parent grading and identifies the compact parent-typical band with the canonical common source for every positive tolerance.
Neither a repair scale nor a tolerance is chosen in this existence statement. The frame's transparent constructor builds an IntegerStep once those parameters satisfy its explicit scalar size test. No hypothesis about output copies, entropy rates, or the final recursive budget is assumed.
import Definitions.Def_mme_released_positive_integer_frame_data set_option autoImplicit false
theorem mme_released_positive_integer_frame (region : Fin 6) (k : ℕ) (hk : 0 < k) :
Nonempty (MME.ReleasedPositiveInteger.Frame region k) := by sorry