realizedClosedScaleModel_of_minimalOrbit
plain-language theorem explainer
From a minimal closed-scale orbit on a closed observable framework one builds the older realized closed-scale model, with closedness and growth now theorem-backed rather than free fields. Hierarchy and forcing authors cite it to pass minimal-orbit data into the realized-model API. The body is a field-by-field record constructor plus one growth lemma.
Claim. Given a closed observable framework $F$ and a minimal closed-scale orbit $O$ on $F$ (base state, positive amplitude, minimal geometric hierarchy, and realization of the ratio orbit), there is a realized closed-scale model for $F$ with the same base state and amplitude, the hierarchy's scale sequence (closed by minimality), growth from the orbit-growth lemma, and the same realization map.
background
The Unified Forcing Chain module aims to force T0–T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). In that setting one works with a closed observable framework: a state space $S$, dynamics $T$, and positive ratio observable $r$ with nontrivial range and no external input.
A minimal closed-scale orbit packages a base state, positive amplitude, a minimal geometric hierarchy, and the statement that the orbit ratios equal amplitude times the hierarchy scales. Growth and closedness are not free data; they come from the minimal hierarchy.
The older interface is a realized closed-scale model: base state, amplitude, a geometric scale sequence that is closed, a growth certificate, and a realization map. Cosmology-side scales are the $\varphi$-powers $\varphi^k$. This definition is the adapter from the newer minimal-orbit package into that older model type.
proof idea
Pure record construction. Copy baseState, amplitude, and amplitude_pos from the orbit; take scales from the embedded minimal hierarchy and scales_closed from its minimal-closure proof; set growth by applying minimalClosedScaleOrbit_growth to $F$ and $O$; copy realize from the orbit. No further tactics.
why it matters
It is the bridge that lets minimal-orbit data feed theorems still typed against realized closed-scale models. Downstream, admissibleOrbitReflection_of_minimalClosedScaleOrbit obtains the admissible-orbit reflection by applying the realized-model reflection lemma to this construction. The same object appears in MinimalClosedScaleOrbitBridge and canonical_minimal_closed_scale_orbit_bridge, which package minimal orbit, realized model, admissible orbit, and $\varphi$-uniform normal form as one equivalence.
In the forcing chain this supports hierarchy realization on closed frameworks without re-proving closedness and growth at each call site. It sits under the discrete ledger and $\varphi$-ladder story (T6 self-similarity, geometric scales as $\varphi^k$), not under a new physical law. No open scaffold: the definition is complete once a MinimalClosedScaleOrbit is supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.