Exact supported child words for every compact released frame
Provedmme_released_positive_frame_supported_child_wordsFor every released inner region r and every natural-number scale k, any compact positive integer frame admits three physical fine words x_0, x_1, x_2 with the exact central child histograms. Write x_i(q) for the numeric entry in mode i at physical coordinate q, and C_i(c,w) for the number of split positions in cell c carrying child word w. Then
Here the split uses the frame's own position enumeration, and mu is the released compact central profile. Every split child word also has the grade prescribed by its cell.
The result keeps the reference address and enumeration already chosen by the frame. It assumes neither a tolerance nor a repair budget, and it handles cells of zero mass. It is conditional on the supplied frame; it does not assert that a frame exists at scale zero. Positive-scale frame existence is a separate accepted theorem.
Exact histograms imply membership in every central child window of nonnegative radius for a step constructed from the same frame. This supplies the supported-window witness used to prove that a graded tolerance stage has at least one type. The theorem does not assert a matrix-volume bound or complete the recursive joint construction.
import Definitions.Def_mme_released_positive_integer_frame_data open BigOperators MME MME.RecursiveYZ MME.CompleteSplit MME.RegionRealization MME.ProfiledCW MME.RecursiveYZ.CWCells MME.ReleasedPositiveInteger set_option autoImplicit false
theorem mme_released_positive_frame_supported_child_words (region : Fin 6) (k : ℕ) (frame : Frame region k) :
∃ x : Fin 3 → FineWord (ReleasedJointInterior.blocks region k * 4),
supported x ∧ ∀ i,
Graded (RecStage.htotal3 region) i frame.reference
(split (ell := 2) frame.positions (ReleasedJointInterior.positions_length region k) (x i)) ∧
Useful (fullCell (RecStage.htotal3 region) frame.reference)
(fun c w => k * RecStage.mu3 region i c w)
(split (ell := 2) frame.positions (ReleasedJointInterior.positions_length region k) (x i)) := by sorry