MinimalOrbitRealizationBridge
plain-language theorem explainer
Certificate that a fixed-data orbit realization of a minimal hierarchy agrees with the canonical level sequence and factors through the closed-scale orbit bridge. Downstream T5→T6 self-similarity and amplitude-normalization cite it. Definitional Prop-structure with two fields; propositional uniqueness is a Subsingleton instance by reflexivity.
Claim. Fix a closed observable framework $F$, a base state $s\in F.S$, an amplitude $a>0$, a minimal hierarchy $H$, and a realization of the orbit of $s$ at scale $a$. A minimal-orbit realization bridge asserts: (i) for every $k$, the observable ratio $F.r(F.T^{[k]}s)$ equals the canonical minimal-orbit level at $k$; (ii) the induced minimal closed-scale orbit satisfies the closed-scale orbit bridge package (normal-form equivalence and admissible reflection).
background
The Unified Forcing Chain module aims to force T0–T8 from the Recognition Composition Law plus normalization and calibration. The present certificate sits in the hierarchy-dynamics layer that feeds the T5→T6 step (unique $J$ to self-similar $\varphi$).
A closed observable framework supplies a state space $S$, a discrete evolution $T$, and a positive ratio observable $r$ with nontrivial range and no external input. A minimal closed-scale orbit packages a base state, positive amplitude, and a minimal hierarchy so that orbit ratios equal amplitude times hierarchy scales. The fixed-data realization certificate isolates that equality as a Prop on given data.
The closed-scale orbit bridge then packages normal-form equivalence of the realized model with admissible orbit reflection. Canonical level sequences are the target comparison object against which a concrete realization is checked.
proof idea
Definitional structure, not a proved theorem. The two fields are pure Prop obligations: pointwise agreement of orbit ratios with the canonical level sequence, and membership of the induced closed-scale orbit in the already-closed bridge package (via the constructor that builds a closed-scale orbit from a realization).
The accompanying Subsingleton instance is a one-line reflexivity proof: any two certificates for the same fixed data are definitionally equal as inhabitants of a Prop-valued structure.
why it matters
This bridge is the interface between raw fixed-data orbit realization and the closed-scale route used by amplitude normalization and the T5→T6 self-similarity certificate. Downstream, the canonical minimal-orbit framework bridge and the unit-amplitude framework bridge inhabit this type, and CanonicalAmplitudeNormalization routes unit-amplitude canonicity through it.
In the forcing chain, T5 uniqueness of $J$ alone does not force $\varphi$; the T5→T6 bridge explicitly records that realized hierarchy data (ratio self-similarity, additive posting) must be supplied. This certificate is part of that hierarchy package: it ensures a realized minimal orbit is not an ad-hoc sequence but the canonical one, projected into the closed-scale bridge. Without it, amplitude gauge and self-similar scale ratio would not share a common realization path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.