minimalOrbitRealization_of_minimalClosedScaleOrbit
plain-language theorem explainer
Any minimal closed-scale orbit on a closed observable framework yields a fixed-data realization certificate: the orbit of the base state matches the scaled minimal hierarchy at every iterate. Hierarchy and scale-forcing arguments cite this projection when they need only the realization equation, not the full orbit bundle. The proof is a one-line field projection.
Claim. Let $F$ be a closed observable framework and let $O$ be a minimal closed-scale orbit on $F$ (base state $s_0$, amplitude $A>0$, and a minimal geometric hierarchy $H$). Then the fixed-data realization certificate holds: for every $k\in\mathbb{N}$, $F.r(F.T^{[k]}(s_0))=A\cdot H.\mathrm{scale}(k)$.
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the Recognition Composition Law, normalization, and calibration. Near the geometric end of that chain one needs discrete scale hierarchies realized by closed dynamical systems.
A closed observable framework supplies a state space $S$, an evolution $T:S\to S$, and a positive observable $r:S\to\mathbb{R}_{>0}$, with nontriviality and finite-description constraints (no external input, countable states). A minimal closed-scale orbit packages a base state, a positive amplitude, a minimal hierarchy, and the pointwise matching law $r(T^{[k]}s_0)=A\cdot\mathrm{scale}(k)$.
The companion structure MinimalOrbitRealization freezes base state, amplitude, and hierarchy as parameters and retains only that matching law as a proposition. Growth and closedness are not extra fields; they are inherited from the minimal hierarchy data.
proof idea
Term-mode structure construction. The goal is a MinimalOrbitRealization at the orbit's base state, amplitude, and minimal hierarchy. The single field realize is filled by projecting the same field from the given MinimalClosedScaleOrbit. No further lemmas are invoked.
why it matters
In the forcing chain, discrete self-similar scale structure (toward T6 $\varphi$ and the eight-tick/D=3 package T7–T8) must be realized inside a closed observable dynamics, not merely postulated as abstract scales. This theorem separates the realization equation from the rest of the orbit bundle, so later arguments can quote a pure Prop certificate at fixed data.
The module doc frames the stronger claim as complete inevitability from cost; isolating realization is the bookkeeping step that keeps hierarchy minimality and dynamical embedding cleanly typed. No downstream users are recorded yet; the declaration is infrastructure for scale-orbit forcing rather than a cited leaf theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.