minimalOrbitRealization_eq_canonical_levels
plain-language theorem explainer
A fixed-data orbit realization forces observable ratios along the dynamical orbit to equal the canonical minimal-orbit level sequence at every step. Hierarchy and closed-scale bridge arguments cite it when converting a realization certificate into sequence-level equalities. The proof is a one-line projection of the realization field, using definitional equality with the canonical levels.
Claim. Let $F$ be a closed observable framework with state space $S$, dynamics $T$, and positive ratio map $r$. Fix a base state $s\in S$, an amplitude $A\in\mathbb{R}$, and a minimal discrete hierarchy $H$. If the orbit of $s$ realizes the scaled hierarchy—i.e. $r(T^k(s))=A\cdot\mathrm{scale}_H(k)$ for every $k$—then $r(T^k(s))$ equals the canonical minimal-orbit level sequence built from $A$ and $H$ at each $k$.
background
This sits in the Unified Forcing Chain module, which derives T-1 through T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The local goal is to connect discrete geometric hierarchies to closed dynamical orbits without free realization data.
A closed observable framework supplies a state type $S$, an endomorphism $T$, and a positive real observable $r$, with nontriviality and no external input. A minimal hierarchy is a geometric scale ladder closed under the first nontrivial composition step (Fibonacci-type closure). The structure MinimalOrbitRealization packages the only remaining map field: the orbit ratios equal amplitude times the hierarchy scales at every iterate.
The companion sequence canonicalMinimalOrbitLevels is the fixed, data-determined level list built from that same amplitude and hierarchy. Upstream scale ladders (including $\phi^k$ forms in large-scale structure) supply the geometric backbone; this lemma only equates a certified orbit to that canonical list.
proof idea
Term-mode one-liner. The hypothesis is a MinimalOrbitRealization certificate whose sole field asserts
$\forall k,; r(T^k(s))=A\cdot\mathrm{scale}_H(k)$.
The goal replaces the right-hand side by canonicalMinimalOrbitLevels A H k. Those two expressions are definitionally equal by construction of the canonical levels, so projecting the certificate field (realization.realize) discharges the goal with no further rewriting or case analysis.
why it matters
This is the equality hinge between a propositional realization certificate and the concrete sequence used by the closed-scale orbit route. Downstream, canonical_minimal_orbit_realization_bridge consumes it to build the canonical bridge from fixed-data orbit realization into the minimal closed-scale orbit pathway (with positivity of amplitude).
In the forcing chain, minimal closed geometric hierarchies encode the self-similar ladder that later pins $\phi$ (T6) and the discrete octave structure (T7/T8). Without matching orbit ratios to a unique canonical level sequence, hierarchy realization would remain an open map rather than a forced identification. The lemma closes that identification for fixed data and keeps the Complete Inevitability Chain free of extra realization choices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.