admissibleOrbit_canonical_growth
plain-language theorem explainer
An admissible orbit on a closed observable framework yields the canonical growth orientation on its multilevel composition: the first orbit step strictly increases the observable. Anyone assembling the φ-uniform normal form from orbit data cites this. The proof is a short rewrite of the orbit-growth inequality into level order via positivity of the ratio map.
Claim. Let $F$ be a closed observable framework (state space $S$, dynamics $T$, positive observable $r$) and let $\mathrm{base}\in S$. If the orbit of $\mathrm{base}$ is admissible in the reflection sense (in particular $1 < r(T(\mathrm{base}))/r(\mathrm{base})$), then the multilevel composition built from that orbit is canonically growth-oriented: its level $0$ is strictly less than its level $1$.
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the Recognition Composition Law, normalization, and calibration. Near T6, discrete self-similar orbits must be identified with the φ-uniform hierarchy.
A closed observable framework supplies a state type $S$, an endomorphism $T$, and a strictly positive real observable $r$, with nontrivial range and no external moduli. AdmissibleOrbitReflection packages the missing orbit data on a chosen base: first-step growth $1 < r(T,\mathrm{base})/r(\mathrm{base})$, constant adjacent ratios (self-similarity), and seed-posting structure. That reflection is what turns a bare closed framework into φ-uniform normal form.
CanonicalGrowthOrientation is the order-level certificate on a nontrivial multilevel composition: levels satisfy $\mathrm{levels},0 < \mathrm{levels},1$. It replaces a divided ratio-greater-than-one hypothesis with a pure comparison of successive levels.
proof idea
Term-mode structure instance: only base_step_grows must be filled. Unfold the multilevel levels so the goal is $r(T^{[0]},\mathrm{base}) < r(T^{[1]},\mathrm{base})$. Rewrite via one_lt_div₀ using positivity of $r$ at the base, converting the strict inequality into $1 < r(T,\mathrm{base})/r(\mathrm{base})$. Discharge by simpa from the orbit_growth field of the admissibility reflection. No further lemmas are needed.
why it matters
This is the growth half of the bridge from admissible orbits to the φ-ladder normal form inside the forcing chain. Downstream, canonical_admissible_orbit_normal_form_reflection installs it as the growth field of the normal-form certificate; admissibleOrbit_canonical_base_ratio_phi then pins the canonical base ratio to φ; and admissibleOrbit_levels_eq_phiUniform equates orbit levels with the φ-uniform composition.
In primer terms this supports T6 (φ forced as the self-similar fixed point): once growth orientation and ratio self-similarity sit on a closed framework orbit, the unique positive self-similar scale is φ. Without this orientation lemma the normal-form reflection cannot be assembled, and the orbit-to-φ identification stalls.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.