canonical_minimal_orbit_realization_bridge
plain-language theorem explainer
Any fixed-data certificate that a closed observable framework's orbit realizes a minimal geometric hierarchy upgrades to a full minimal-orbit realization bridge: the orbit matches the canonical level sequence and projects to a minimal closed-scale orbit. Cited by anyone assembling the T5→T6 self-similarity step in the unified forcing chain. The proof is a two-field term assembly from the equality-to-canonical-levels lemma and the closed-scale orbit bridge.
Claim. Let $F$ be a closed observable framework with state space $S$, dynamics $T$, and positive ratio observable $r$. Fix a base state $s_0\in S$, an amplitude $A>0$, and a minimal discrete hierarchy $H$ (a geometric scale ladder closed under the first nontrivial composition). If the orbit of $s_0$ realizes $H$ at scale $A$, i.e. $r(T^k s_0)=A\cdot\mathrm{scale}_H(k)$ for all $k$, then this realization is a minimal-orbit realization bridge: the realized levels agree with the canonical target sequence, and the data project to a minimal closed-scale orbit for $F$.
background
The module UnifiedForcingChain aims to force the full T0–T8 chain from the Recognition Composition Law plus normalization and calibration. The T5→T6 step needs self-similarity of a discrete ledger hierarchy, which is packaged through closed-scale orbits and their realizations.
A closed observable framework supplies a state space $S$, a dynamics $T:S\to S$, and a positive ratio map $r:S\to\mathbb{R}_{>0}$, with nontrivial observability and no external moduli. A minimal hierarchy is a geometric scale sequence closed under the first nontrivial composition step (the Fibonacci-type closure). A fixed-data orbit realization asserts that the sampled orbit ratios equal amplitude times those scales: $r(T^k s_0)=A\cdot\mathrm{scale}(k)$.
The bridge structure strengthens that certificate: uniqueness of the realization for fixed data, agreement with a canonical sequence-level orbit, and projection into a MinimalClosedScaleOrbit. Upstream, the closed-framework axioms and hierarchy minimality supply the geometric ladder; the realization structure isolates the remaining map field that must match the ladder.
proof idea
Term-mode structure construction with two fields.
canonical_levels is filled by minimalOrbitRealization_eq_canonical_levels, which equates the realized orbit ratios to the canonical target sequence for the given framework and realization certificate.
minimal_orbit_bridge is filled by first converting the fixed-data realization into a minimal closed-scale orbit via minimalClosedScaleOrbit_of_realization (using positivity of the amplitude), then applying canonical_minimal_closed_scale_orbit_bridge to obtain the closed-scale orbit bridge certificate.
No extra case analysis: the hypotheses already pin $A>0$ and the pointwise orbit-scale identity.
why it matters
This lemma is the generic upgrade from a bare orbit-realization Prop to the bridge certificate used throughout the forcing chain. Downstream, canonicalMinimalOrbitFramework_bridge specializes it to the canonical minimal-orbit framework, and t5_to_t6_bridge_holds consumes the realized closed-scale route as one arm of the T5→T6 self-similarity bridge ("The T5-to-T6 self-similarity bridge is theorem-backed").
In the primer landmarks, T5 forces uniqueness of the cost $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger. The bridge ensures that any framework orbit realizing a minimal closed hierarchy is on the canonical closed-scale path that forces $\varphi$, rather than an ad hoc ladder. It closes a packaging gap between fixed-data realization certificates and the hierarchy-dynamics lemmas that feed the complete inevitability chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.