RealizedClosedScaleAdmissibleOrbitBridge
plain-language theorem explainer
Packages three certificates into one Prop: a realized closed-scale model admits an orbit with growth and ratio self-similarity, that orbit yields the φ-uniform normal form, and the direct closed-scale normal-form equivalence agrees. Cited by the T5→T6 self-similarity bridge and the minimal closed-scale orbit package. Pure structure definition; uniqueness is propositional (Subsingleton).
Claim. For a closed observable framework $F$ and a realized closed-scale model $H$ on $F$, the following three data are packaged as one bridge: (i) the base state of $H$ carries an admissible orbit (growth of the first step, constant adjacent ratios, additive seed posting); (ii) that admissible orbit supplies the canonical $\varphi$-uniform normal form (uniform scale law, growth orientation, seed closure); (iii) the direct closed-scale multilevel composition is equivalent to the same normal form.
background
The Unified Forcing Chain module aims to force T0–T8 from the Recognition Composition Law alone. The T5→T6 step needs self-similarity on a discrete ledger to pin $\varphi$ as the unique scale ratio. A bare closed observable framework does not yet carry hierarchy fields (ratio self-similarity, additive posting); those must be supplied explicitly.
An admissible orbit reflection records exactly that missing data on one orbit of the base state: first-step growth $r(T,\mathrm{base})/r(\mathrm{base})>1$, constant adjacent ratios along the orbit, and additive seed posting. From that orbit one builds a multilevel composition and asks for the canonical $\varphi$-uniform normal form (uniform scale law, growth orientation, seed closure). Independently, a realized closed-scale model already has a direct normal-form equivalence certificate of the same shape.
This structure asserts that those three views—admissible orbit, orbit-derived normal form, and direct closed-scale normal form—are one bridge package for fixed $F$ and $H$.
proof idea
Definitional structure, not a proved theorem. The body is the three Prop fields with no further proof obligations at the structure site. A companion Subsingleton instance shows any two inhabitants are definitionally equal (allEq _ _ := by rfl), so the bridge certificate is propositionally unique for fixed data. The canonical inhabitant is constructed downstream by canonical_realized_closed_scale_admissible_orbit_bridge, which fills the three fields from admissibleOrbitReflection_of_realizedClosedScale and the matching normal-form certificates.
why it matters
Sits on the T5→T6 corridor of the forcing chain. Downstream, T5_To_T6_SelfSimilarity_Bridge routes φ-forcing through internal hierarchy dynamics: a closed framework plus realized hierarchy forces the scale ratio to be φ, while recording that bare framework fields alone do not force hierarchy data. This package is the intermediate glue that makes that route honest—no smuggled self-similarity.
It is also consumed by MinimalClosedScaleOrbitBridge, which collapses minimal closed-scale orbit, realized model, admissible orbit, and φ-normal form into one certificate, and by the canonical constructor that witnesses the package is inhabited whenever a realized closed-scale model exists.
Framework landmark: T6 (φ forced as the self-similar fixed point of the discrete ledger). The structure does not itself force φ; it standardizes the bridge data the T5→T6 certificate needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.