minimalClosedScaleOrbit_of_realization
plain-language theorem explainer
From a fixed-data orbit-realization certificate one obtains a minimal closed-scale orbit: base state, positive amplitude, minimal geometric hierarchy, and the pointwise scale-matching law. Anyone assembling the T6–T8 ladder inside a closed observable framework cites this packing step. The body is a pure field projection: copy data and take the certificate’s realize map.
Claim. Given a closed observable framework $F$ with dynamics $T$ and positive observable $r$, a base state $s_0\in F.S$, an amplitude $A>0$, a minimal closed geometric hierarchy $H$, and a certificate that $r(T^k s_0)=A\cdot\mathrm{scale}_H(k)$ for every $k$, there is a minimal closed-scale orbit on $F$ with those same data and that same realization identity.
background
The module UnifiedForcingChain aims at a complete inevitability chain from the cost foundation (Recognition Composition Law plus normalization and calibration) through T-1 to T8, including $\varphi$ forced by self-similarity and the eight-tick octave with $D=3$.
A closed observable framework supplies a state space $S$, an evolution $T:S\to S$, and a strictly positive observable $r$ with at least two distinct values, under closure and finite-description constraints. A minimal hierarchy is a geometric scale ladder closed under the first nontrivial composition step (Fibonacci-type closure).
MinimalClosedScaleOrbit packages base state, positive amplitude, such a hierarchy, and the orbit law $r(T^k s_0)=A\cdot\mathrm{scale}(k)$. The sibling certificate MinimalOrbitRealization isolates only that realize field for fixed data, so growth and closedness need not be re-proved here; they ride on the hierarchy.
proof idea
Definitional constructor, not a tactic proof. Instantiate MinimalClosedScaleOrbit by setting base state, amplitude, positivity, and minimal hierarchy to the supplied arguments, and set the realize field equal to the certificate’s realize map. No lemmas are applied; the type of the certificate already guarantees the required $\forall k$ identity.
why it matters
This is the projection half of the orbit-realization bridge used later in the forcing chain. Downstream, MinimalOrbitRealizationBridge records that fixed-data realization is unique, projects to a minimal closed-scale orbit, and agrees with the canonical sequence-level orbit; canonical_minimal_orbit_realization_bridge is the corresponding theorem-shaped bridge.
In the T0–T8 story the object matters once discrete self-similar scales must sit inside a closed framework: T6 forces $\varphi$ as the self-similar fixed point, and the geometric ladder feeds the eight-tick / $D=3$ steps. Isolating realization as a Prop certificate keeps the orbit data reusable without reopening hierarchy minimality. The packing itself closes no open forcing gap; it only standardizes the data shape those bridges consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.