minimalClosedScaleOrbit_growth
plain-language theorem explainer
Any minimal closed-scale orbit has scale ratio strictly greater than one. Hierarchy and closed-observable constructions cite this to guarantee genuine geometric growth rather than a fixed or contracting ladder. The proof rewrites the ratio as φ via hierarchy minimality, then applies φ > 1.
Claim. Let $F$ be a closed observable framework and let $O$ be a minimal closed-scale orbit in $F$. Then the scale ratio of the underlying minimal hierarchy satisfies $1 < O.\mathrm{minimal}.\mathrm{scales}.\mathrm{ratio}$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law, normalization, and calibration. In that setting a closed observable framework supplies a state space, a dynamics $T$, and a positive observable $r$ with nontrivial range and no external input.
A minimal closed-scale orbit packages a base state, a positive amplitude, and a MinimalHierarchy, together with a realization identity: iterating $T$ multiplies the observable by amplitude times the hierarchy scale at step $k$. Growth and closedness are not extra fields; they are meant to follow from minimality of the hierarchy.
Upstream, hierarchy_forces_phi states that minimal closure already forces the unique positive self-similar ratio $\varphi$. The classical scale ladder is $\mathrm{scale}(k)=\varphi^k$. The present lemma isolates the growth half of that package: the forced ratio exceeds one.
proof idea
Term-mode, three steps. Apply HierarchyMinimality.hierarchy_forces_phi to O.minimal to obtain equality of the hierarchy scale ratio with $\varphi$. Rewrite the goal along that equality. Finish with PhiForcing.phi_gt_one, which supplies $1 < \varphi$. No case split or induction.
why it matters
In the forcing chain, T6 pins $\varphi$ as the self-similar fixed point of the discrete ledger. This theorem turns that uniqueness into a strict growth inequality for every minimal closed-scale orbit, so the geometric hierarchy cannot be stationary or contracting.
The sole downstream consumer is realizedClosedScaleModel_of_minimalOrbit, which builds the older realized closed-scale model from a minimal orbit "with closedness and growth now theorem-backed." Without this inequality that constructor could not honestly claim growth.
It sits between hierarchy minimality (ratio equals $\varphi$) and the concrete realization interface used later in the chain. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.