admissibleOrbit_levels_eq_phiUniform
plain-language theorem explainer
An admissible orbit in a closed observable framework is level-equivalent to its φ-uniform normal form: ratios along the orbit equal the levels of the φ-uniform multilevel composition built from that orbit. Anyone packaging the canonical admissible-orbit normal-form certificate cites this. The proof is a short term application of uniqueness for φ-uniform closed levels, fed by the orbit's canonical uniformity, growth, and seed size.
Claim. Let $F$ be a closed observable framework with state space $S$, evolution $T$, and positive ratio observable $r$. Fix a base state that carries an admissible orbit reflection (first step grows; adjacent orbit ratios are self-similar). Then for every $k$, $r(T^{k}(\mathrm{base}))$ equals the $k$-th level of the $\varphi$-uniform closed multilevel composition of the admissible-orbit multilevel composition of $F$ at that base.
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. Here the local objects are closed observable frameworks: a state type $S$, an evolution $T:S\to S$, and a strictly positive ratio observable $r$, with nontrivial observability and no external input.
An admissible orbit reflection supplies the exact data a bare closed framework lacks for φ-normal form: the first orbit step grows ($1 < r(T,\mathrm{base})/r(\mathrm{base})$), and adjacent ratios are self-similar along the whole orbit. From that data one builds an admissible-orbit multilevel composition and compares it to the φ-uniform closed multilevel composition of the same seed.
Upstream, the three canonical lemmas already convert admissibility into the growth orientation, uniformity, and seed-size hypotheses that the uniqueness theorem for φ-uniform closed levels expects. Those lemmas are the direct inputs here.
proof idea
Term-mode one-shot application of phiUniformClosed_levels_unique. Both composition arguments are the admissible-orbit multilevel composition of $F$ at the base (identity via rfl). The three remaining hypotheses are discharged by admissibleOrbit_canonical_uniform, admissibleOrbit_canonical_growth, and admissibleOrbit_canonical_seed_size, each applied to the same admissible-orbit reflection certificate. No further case splits or induction.
why it matters
This is the level-matching half of the admissible-orbit normal-form story inside the forcing chain. Downstream, canonical_admissible_orbit_normal_form_reflection packages the full certificate ("The canonical admissible-orbit normal-form reflection certificate"), of which level-equivalence is the content that says the orbit really is the φ-uniform ladder, not merely growth-oriented.
In framework terms this sits under T6 (φ forced as the self-similar fixed point of the discrete ledger): once an orbit is admissible, its observable levels are forced to the unique φ-uniform schedule. That normal form is what later steps use when reading rung structure, eight-tick cadence (T7), and dimensional forcing (T8) off a single closed dynamics. Without level-equivalence, admissibility would only give qualitative growth, not the quantitative φ-ladder identification the chain needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.