canonicalMinimalOrbitFramework_realization
plain-language theorem explainer
The canonical minimal-orbit framework, built from a positive amplitude and a minimal geometric hierarchy, realizes that hierarchy along the orbit starting at natural zero: the observable at the k-fold iterate equals amplitude times the k-th scale. Anyone wiring T5–T6 self-similarity or amplitude-normalization certificates cites this. The proof is a short term argument: after identifying succ-iterates of zero with k, the equality is definitional.
Claim. For every positive real amplitude $A>0$ and every minimal discrete hierarchy $H$ (a geometric scale ladder closed under the first nontrivial composition), the canonical minimal-orbit framework built from $A$ and $H$ realizes $H$ from base state $0$: for all $k\in\mathbb{N}$, the framework observable at the $k$-fold iterate of the dynamics equals $A\cdot H.\mathrm{scales}(k)$.
background
This lives in the Unified Forcing Chain module, which aims to force T0–T8 from the cost foundation (Recognition Composition Law, normalization, calibration). The local step is the passage from a closed observable framework plus hierarchy data toward self-similarity and $\varphi$ (the T5→T6 bridge).
A MinimalHierarchy is a geometric scale sequence closed under the first nontrivial composition step (the Fibonacci-type closure). MinimalOrbitRealization is a fixed-data certificate: for framework $F$, base state $s$, amplitude $A$, and hierarchy $H$, one needs $\forall k,, F.r(F.T^{[k]} s)=A\cdot H.\mathrm{scales}.\mathrm{scale},k$. That isolates the remaining realization map field of a minimal closed scale orbit.
Upstream, scales are geometric (e.g. powers of $\varphi$ in related cosmology scaffolding), successor is the generator of the logic-derived naturals, and canonical arithmetic supplies the initial Peano object. The theorem only needs that iterating successor from $0$ recovers the index $k$.
proof idea
Term-mode proof of the single realize field. Introduce $k$, then change the goal to the explicit level equation: the canonical minimal-orbit levels at $((\mathrm{Nat.succ})^{[k]}),0$ equal amplitude times the $k$-th minimal scale. Rewrite with nat_succ_iterate_zero (so the iterated successor of zero is $k$), then close by rfl: the canonical framework is defined so the equality holds definitionally once the index is $k$.
why it matters
This is the definitional realization pin for the canonical minimal-orbit framework: without it, bridges that project the framework into a full minimal-orbit realization certificate cannot fire. Downstream it feeds canonicalMinimalOrbitFramework_bridge, the unit-amplitude bridge, and CanonicalAmplitudeNormalization (amplitude as positive scalar gauge, unit framework canonical).
It also sits under T5_To_T6_SelfSimilarity_Bridge: that certificate routes T5 J-uniqueness into hierarchy dynamics forcing the scale ratio to be $\varphi$, while recording that bare closed-framework fields do not smuggle hierarchy data. Landmark-wise this is infrastructure for T6 ($\varphi$ as self-similar fixed point) after T5 (unique $J$), not a new forcing step by itself. No scaffolding remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.