admissibleOrbit_ratio_eq_base
plain-language theorem explainer
In any closed observable framework, an admissible orbit has constant adjacent scaling: every successive ratio of the observable equals the base step ratio. Anyone deriving φ-uniform normal form from ledger dynamics cites this. The proof is a short induction that unfolds the self-similarity clause of admissibility.
Claim. Let $F$ be a closed observable framework with state space $S$, transition $T$, and positive observable $r$. Fix a base state $b\in S$ and an admissible orbit reflection at $b$ (growth of the first step, and self-similarity of adjacent ratios). Then for every $k\in\mathbb{N}$, $$\frac{r(T^{k+1}b)}{r(T^{k}b)}=\frac{r(Tb)}{r(b)}.$$
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. Closed frameworks supply the dynamical setting: a type of states $S$, a transition $T:S\to S$, and a strictly positive real observable $r$, with nontriviality and no external input.
Admissible orbit reflection packages the exact extra data missing from a bare closed framework: the first orbit step must grow, and adjacent ratios must be self-similar, $$\frac{r(T^{k+2}b)}{r(T^{k+1}b)}=\frac{r(T^{k+1}b)}{r(T^{k}b)}.$$ That reflection property is what turns a closed framework into the $\varphi$-uniform normal form used later in the forcing chain (T6 self-similarity on the discrete ledger).
The present lemma upgrades pairwise self-similarity to global constancy of the ratio along the whole orbit, equal to the base ratio $r(Tb)/r(b)$.
proof idea
Term-mode induction on the orbit index $k$.
- Zero case: both sides are the base ratio, so
rfl. - Successor: invoke the admissibility field
orbit_ratio_self_similarat $k$, which equates the $(k+2)/(k+1)$ ratio with the $(k+1)/k$ ratio; rewrite by that equality and the inductive hypothesis to collapse to the base ratio.
No external lemmas beyond the structure fields of admissibility and the closed-framework interface.
why it matters
This is the bridge from local self-similarity of an admissible orbit to a single global scale factor. Downstream, admissibleOrbit_canonical_uniform quotes it (via multilevel composition) to obtain a canonical uniform scale law: "An admissible orbit directly supplies canonical uniform scaling."
In the forcing chain that is the T6 step: $\varphi$ is forced as the self-similar fixed point of discrete ledger dynamics. Constant adjacent ratios are exactly the geometric progression whose growth rate is later identified with $\varphi$ under the Recognition Composition Law and calibration. Without constancy of ratios, uniform scaling (and thus the $\varphi$-ladder mass and tick structure) would not be forced from admissibility alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.