AdmissibleOrbitReflection
plain-language theorem explainer
Packages the three orbit conditions a closed observable framework needs beyond bare closure: first-step growth, constant adjacent ratios, and additive seed posting at step two. Anyone proving φ-uniform normal form or T6 self-similarity cites this certificate. It is a pure Prop structure (definitional data), with a Subsingleton instance so certificates are unique up to proof irrelevance.
Claim. For a closed observable framework $F$ (state space $S$, step map $T$, positive observable $r$) and base state $b\in S$, an admissible-orbit reflection is the conjunction of: (i) growth $1 < r(T b)/r(b)$; (ii) self-similarity of adjacent ratios, $r(T^{k+2}b)/r(T^{k+1}b)=r(T^{k+1}b)/r(T^k b)$ for all $k$; (iii) additive seed posting $r(T^2 b)=r(T b)+r(b)$.
background
The module UnifiedForcingChain aims to force the full T0–T8 chain from the Recognition Composition Law plus normalization and calibration. T6 is the step that pins $\varphi$ as the unique self-similar fixed point of a discrete ledger orbit.
A closed observable framework supplies only a state type $S$, an endogenous step $T:S\to S$, and a strictly positive real observable $r$, with nontriviality (two states of unequal $r$). That is enough for closure and observability, but not enough to force geometric growth: one still needs an orbit that grows, keeps a constant scale factor, and posts its seed additively.
Those three missing conditions are exactly the reflection data. Once present, the orbit can be read as a multilevel composition and matched to the $\varphi$-uniform normal form used throughout the forcing chain.
proof idea
Definitional structure, not a derived theorem. The three fields are Prop-valued hypotheses on iterates of $T$ under $r$; there is no tactic proof body beyond the structure declaration itself.
A companion Subsingleton instance records propositional uniqueness: any two certificates for fixed $F$ and base are definitionally equal (allEq by rfl), so downstream lemmas may treat the certificate as unique data rather than a choice.
why it matters
This is the interface that turns a bare closed framework into the $\varphi$-ladder input for T6. Downstream, admissibleOrbit_canonical_growth, admissibleOrbit_canonical_uniform, and admissibleOrbit_canonical_seed_size read the three fields straight into the canonical growth, uniform-scale, and seed-size laws. From those, admissibleOrbit_canonical_base_ratio_phi concludes the canonical base ratio equals $\varphi$, and admissibleOrbit_levels_eq_phiUniform equates every orbit level to the $\varphi$-uniform multilevel composition.
AdmissibleOrbitNormalFormReflection then bundles the full normal-form certificate on top of this structure. In the forcing chain language: without growth + ratio self-similarity + additive posting, the self-similar fixed-point argument that forces $\varphi$ (T6) does not fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.