realizedClosedScaleMultilevelComposition
plain-language theorem explainer
A realized closed-scale model on a closed observable framework yields a nontrivial multilevel composition by reading the scale observable along the orbit of the base state. Hierarchy and φ-uniformity lemmas cite this packaging rather than a full RealizedHierarchy wrapper. The body is definitional: levels are successive radii under the framework dynamics, with positivity discharged by the framework's radius positivity.
Claim. Given a closed observable framework $F$ and a realized closed-scale model $H$ for $F$, the sequence $\ell(k) = r(T^{k}(s_0))$ (base state $s_0$, dynamics $T$, scale observable $r$) is a nontrivial multilevel composition: every level is positive, and at least the first three levels are positive.
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. Downstream of unique $J$ and forced $\varphi$ (T5–T6), one needs a clean interface from closed-scale realizations to multilevel hierarchy data.
A closed observable framework supplies a dynamics $T$, a scale (radius) observable $r$, and a positivity witness $r>0$ on states. A realized closed-scale model packages a base state whose orbit under $T$ is the closed-scale realization. Multilevel composition is the hierarchy-forcing interface: a sequence of positive real levels with a nontriviality side condition (at least three positive levels).
This definition skips packaging the orbit as a full RealizedHierarchy and exposes the orbit radii directly as that multilevel sequence. Related cost algebra uses the shifted cost $H(x)=J(x)+1$, under which RCL becomes d'Alembert form; the present object is geometric/scale-side, not a redefinition of $J$.
proof idea
Structure construction, not a deep proof. The levels field is $\lambda k., r(T^{[k]}(s_0))$. Positivity of every level is exact on the framework's $r_\mathrm{pos}$. The at-least-three witness is three nested constructors, each again $r_\mathrm{pos}$ on the corresponding orbit point. No external lemmas beyond the framework interface.
why it matters
This is the bridge from closed-scale realization into hierarchy forcing without an intermediate RealizedHierarchy package. Downstream, it is the subject of canonical uniform scale law, canonical growth orientation, canonical seed-size law, and the theorem that the canonical base ratio equals $\varphi$. Levelwise equality to the $\varphi$-uniform normal form and the RealizedClosedScaleNormalFormEquivalence certificate both quantify over this composition.
In the forcing chain, that lands next to T6 ($\varphi$ as self-similar fixed point) and the discrete ledger/scale ladder that feeds T7–T8. The doc-comment on the uniform law states the intent: a realized closed-scale model directly supplies the canonical uniform law. Without this def, those φ-normal-form comparisons would have to rebuild the orbit packaging at each call site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.