MinimalOrbitRealization
plain-language theorem explainer
A fixed-data certificate that an orbit under a closed observable framework realizes a minimal geometric hierarchy: the ratio observable along iterates of the base state equals a positive amplitude times the hierarchy scale at each step. Isolates the single realization equation that remains after packaging growth and closedness into MinimalHierarchy. Cited by the T5-to-T6 self-similarity bridge and by constructors that rebuild MinimalClosedScaleOrbit. Definitional structure plus a Subsingleton instance (propositional uniqueness).
Claim. Given a closed observable framework $F$ (state space $S$, evolution $T$, positive ratio observable $r$), a base state $s_0\in S$, an amplitude $A\in\mathbb{R}$, and a minimal discrete hierarchy $H$ (geometric scale ladder closed under the first nontrivial composition), the orbit-realization certificate asserts $$\forall k\in\mathbb{N},\quad r(T^k s_0)=A\cdot\mathrm{scale}_H(k).$$ For fixed $(F,s_0,A,H)$ any two such certificates are propositionally equal.
background
The Unified Forcing Chain module aims to force T0–T8 from the Recognition Composition Law plus normalization and calibration. The T5→T6 step needs self-similarity on a discrete ledger: a geometric scale ladder whose first nontrivial closure is the Fibonacci relation, realized as an orbit of observables.
A closed observable framework supplies a state type $S$, an evolution map $T:S\to S$, and a strictly positive ratio observable $r:S\to\mathbb{R}$, with nontriviality (two states of unequal $r$) and no external input. A minimal hierarchy packages a geometric scale sequence together with the closedness witness; growth and closedness are not separate fields once that package is fixed.
MinimalClosedScaleOrbit bundles base state, positive amplitude, the minimal hierarchy, and the realization equation. The present structure peels off only the realization equation as a standalone Prop on fixed data, so uniqueness and bridging lemmas can talk about that field alone.
proof idea
Definitional structure: a single field realize stating pointwise equality of the framework ratio along the $T$-orbit of the base state with amplitude times the hierarchy scale sequence. No proof obligations beyond inhabiting that Prop.
The accompanying Subsingleton instance is immediate: any two certificates are equal by rfl because a Prop-valued structure with one field is unique up to proof irrelevance. Downstream constructors (e.g. building a full minimal closed-scale orbit from this certificate) simply reassemble the peeled fields with a positivity hypothesis on the amplitude.
why it matters
This certificate is the thin interface between hierarchy minimality and concrete framework orbits. Downstream, minimalClosedScaleOrbit_of_realization rebuilds the full minimal closed-scale orbit; canonicalMinimalOrbitFramework_realization shows the canonical framework realizes its target sequence definitionally from $0$; and minimalOrbitRealization_eq_canonical_levels equates any fixed-data realization with the canonical sequence-level orbit.
The bridge structure MinimalOrbitRealizationBridge packages uniqueness, projection to MinimalClosedScaleOrbit, and canonical agreement. Critically, T5_To_T6_SelfSimilarity_Bridge consumes this realization language: T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger once a minimal closed geometric hierarchy is realized by an orbit. Isolating the realization map keeps the T5–T6 step free of redundant growth/closedness bookkeeping already discharged by MinimalHierarchy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.