admissibleOrbitMultilevelComposition
plain-language theorem explainer
Packages the orbit of a base state under a closed observable framework's dynamics into a positive multilevel composition with at least three levels. Hierarchy and φ-forcing arguments cite it as the bridge from admissible orbits to the older multilevel interface. The construction sets levels to successive observable ratios and discharges positivity by the framework's built-in ratio positivity.
Claim. Given a closed observable framework $F$ (state space $S$, dynamics $T:S\to S$, positive ratio observable $r:S\to\mathbb{R}$) and a base state $b\in S$, the sequence $\ell(k)=r(T^{k}(b))$ is a nontrivial multilevel composition: every level is strictly positive, and in particular $\ell(0),\ell(1),\ell(2)>0$.
background
The Unified Forcing Chain module aims to force the full T0–T8 ladder from the cost foundation (Recognition Composition Law plus normalization and calibration). Mid-chain, discrete ledger dynamics and observables must be packaged as multilevel compositions so that self-similarity can pin the golden ratio $\varphi$ (T6).
A closed observable framework supplies a state type $S$, an endomorphism $T$, and a strictly positive real observable $r$, with nontriviality ($r$ not constant) and closure (no external moduli). The hierarchy-forcing structure NontrivialMultilevelComposition is simply a map $\mathbb{N}\to\mathbb{R}$ that is pointwise positive and positive on the first three indices; later theorems then force uniform adjacent ratios when free scale parameters are forbidden.
Relatedly, RealizedHierarchy is the RS-native packaging of the same orbit data (base state, levels $r(T^{k}b)$, growth $1<\ell(1)/\ell(0)$). The present definition is the thinner multilevel face of that orbit, enough to feed canonical uniform-scale and seed-size laws.
proof idea
Definitional construction, not a deep proof. Levels are defined by $\ell(k)=r(T^{[k]}(b))$. Pointwise positivity is r_pos applied at each iterate. The three-level witness is three applications of the same positivity fact at $k=0,1,2$. No external lemmas beyond the closed-framework field r_pos.
why it matters
This is the adapter that lets admissible orbits speak the language of hierarchy forcing inside the complete inevitability chain. Downstream, it is the carrier for canonical uniform scaling, growth orientation, seed-size law, and the identification of the canonical base ratio with $\varphi$ (admissibleOrbit_canonical_base_ratio_phi, admissibleOrbit_canonical_uniform, admissibleOrbit_canonical_growth, admissibleOrbit_canonical_seed_size). Levelwise equality to the $\varphi$-uniform normal form and the AdmissibleOrbitNormalFormReflection certificate are built on the same object.
In framework terms it sits on the path to T6 ($\varphi$ forced as the self-similar fixed point) once no-free-scale and seed-closure are imposed on the orbit. It does not itself prove $\varphi$; it supplies the multilevel data those theorems consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.