realizedClosedScale_canonical_growth
plain-language theorem explainer
Any realized closed-scale model on a closed observable framework yields a multilevel composition whose first step strictly grows. Hierarchy and normal-form arguments cite this as the order certificate replacing a bare ratio-greater-than-one hypothesis. The proof rewrites the level comparison into the model's base growth ratio via the closed-scale step identity and positivity of the observable.
Claim. Let $F$ be a closed observable framework and $H$ a realized closed-scale model on $F$. Then the multilevel composition built from $H$ has canonical growth orientation: its level at index $0$ is strictly less than its level at index $1$. Equivalently, $F.r(F.T^{0}(H.\mathrm{base})) < F.r(F.T^{1}(H.\mathrm{base}))$.
background
The module UnifiedForcingChain assembles the complete inevitability chain from the cost foundation (Recognition Composition Law plus normalization and calibration) through T-1 to T8. Within that chain, closed observable frameworks package a discrete dynamical orbit $T$ with a positive real observable $r$ used to read scale.
A realized closed-scale model supplies a base state together with a growth certificate: the ratio of successive observable values along the orbit is forced above one at the seed step. Canonical growth orientation is the order-level packaging of that fact for a nontrivial multilevel composition: it asserts only $\mathrm{levels},0 < \mathrm{levels},1$, the first nontrivial rung larger than the base.
The companion construction realizedClosedScaleMultilevelComposition turns the closed-scale orbit into such a multilevel composition. Upstream ratio-step lemmas identify consecutive level ratios with the model's intrinsic growth data, so orientation becomes a direct readout rather than an extra axiom.
proof idea
Short tactic proof of the single field base_step_grows. Change the goal to the concrete inequality $F.r(F.T^{[0]} H.\mathrm{baseState}) < F.r(F.T^{[1]} H.\mathrm{baseState})$. Rewrite via one_lt_div₀ using positivity of $r$ on the orbit, then apply the closed-scale ratio-step identity at index $0$. The resulting goal is exactly the model's built-in growth hypothesis $H.\mathrm{growth}$, discharged by exact.
why it matters
This lemma is the growth half of the canonical normal-form package for realized closed-scale models. Downstream, canonical_realized_closed_scale_normal_form_equivalence installs it as the growth field beside the uniform certificate, producing the direct equivalence certificate for those models.
It also feeds realizedClosedScale_canonical_base_ratio_phi and realizedClosedScale_levels_eq_phiUniform, which identify the composition's base ratio with $\varphi$ and match orbit levels to the $\varphi$-uniform normal form. In the forcing chain that is the bridge from closed-scale realization data to the T6 self-similar fixed point and the discrete $\varphi$-ladder used for mass and constants.
No scaffolding remains here: the claim is fully proved and only packages existing growth data into the canonical orientation interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.