AdmissibleOrbitNormalFormReflection
plain-language theorem explainer
Packages the full normal-form certificate for an admissible orbit in a closed observable framework: uniform scaling, growth orientation, additive seed law, base ratio equal to φ, levelwise agreement with the φ-uniform hierarchy, and equivalence to the older realized-hierarchy route. Cited by the T5→T6 self-similarity bridge and the closed-scale/admissible-orbit bridge packages. Definitional Prop structure; uniqueness is propositional (Subsingleton).
Claim. Fix a closed observable framework $F$ with base state $b$ and an admissible-orbit reflection $A$ on the orbit of $b$ (growth of the first step, constant adjacent ratios, and the missing admissibility data). An admissible-orbit normal-form reflection is a proposition asserting: the multilevel composition of that orbit obeys the canonical uniform-scale law, growth orientation, and seed-size law; its canonical base ratio equals $\varphi$; every orbit level $r(T^k b)$ equals the $k$-th level of the $\varphi$-uniform normal form; and the induced realized hierarchy is equivalent to that normal form.
background
The module UnifiedForcingChain aims at a complete inevitability chain from the cost foundation (Recognition Composition Law plus normalization and calibration) through T0–T8. The T5→T6 step needs self-similarity that forces the golden ratio $\varphi$ as the discrete ledger scale.
A closed observable framework supplies a state space $S$, a dynamics $T$, and a positive ratio observable $r$, with nontriviality and no external input. Bare closure does not force hierarchy fields. An admissible-orbit reflection adds the missing data on one orbit: first-step growth, ratio self-similarity along the orbit, and (with related packages) additive seed posting. That turns the orbit into a nontrivial multilevel composition.
Canonical certificates then replace raw hypotheses: uniform scale means each adjacent level is the previous times the hierarchy’s own base ratio; growth orientation means level 0 is strictly below level 1; seed size means the canonical seed index posts as the sum of levels 0 and 1. The older realized-hierarchy normal-form equivalence asserts the same package along the realized-hierarchy route.
proof idea
No proof body: this is a Prop-valued structure (definitional certificate bundle), not a derived theorem. Fields are named hypotheses on the multilevel composition built from the admissible orbit of base in $F$. A companion Subsingleton instance shows any two such certificates are propositionally equal (rfl), so the bundle is unique up to proof irrelevance once $F$, base, and the admissibility data are fixed. Inhabitation is supplied downstream by canonical_admissible_orbit_normal_form_reflection, which fills the fields from admissible-orbit canonical uniform/growth lemmas and related constructions.
why it matters
This is the normal-form face of admissible-orbit data in the forcing chain. Downstream, canonical_admissible_orbit_normal_form_reflection builds the canonical inhabitant; RealizedClosedScaleAdmissibleOrbitBridge and MinimalClosedScaleOrbitBridge identify closed-scale models, admissible orbits, and the φ-uniform normal form as one bridge package; T5_To_T6_SelfSimilarity_Bridge routes T5 (unique $J$) into T6 (φ forced by self-similarity on a realized hierarchy), while recording that bare closed-framework fields alone do not force hierarchy structure.
In primer terms it sits on the T5→T6 link: after $J$-uniqueness, discrete self-similar scaling on an admissible orbit pins the base ratio to $\varphi$, the fixed point of the self-similar ladder. It does not itself prove T6; it states the certificate shape those bridges discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.