phiUniformClosed_growth
plain-language theorem explainer
Any nontrivial multilevel hierarchy, rewritten in φ-uniform normal form (base level times φ^k), has strictly growing first step: level 0 is smaller than level 1. Hierarchy and φ-forcing arguments cite this as the growth half of the canonical φ-uniform closure certificate. The proof unfolds the normal form and finishes by nlinarith from positivity of the base and φ > 1.
Claim. Let $M$ be a nontrivial multilevel composition (positive real levels with at least three levels). Form its $\varphi$-uniform normal form by $k \mapsto M.{\rm levels}(0)\cdot\varphi^k$. Then this normal form is 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 plus normalization and calibration. T6 is the step that forces $\varphi$ as the self-similar fixed point of the discrete ledger.
A nontrivial multilevel composition is a positive real sequence of levels with at least three entries. Canonical growth orientation is the order-level certificate that the first nontrivial level exceeds the base: ${\rm levels}(0) < {\rm levels}(1)$. It replaces a divided ratio-greater-than-one hypothesis.
The $\varphi$-uniform normal form keeps the original base and multiplies by powers of $\varphi$: ${\rm levels}_\varphi(k) = M.{\rm levels}(0)\cdot\varphi^k$. The associated multilevel composition packages that sequence with positivity and the three-level witness. This theorem asserts that the packaged normal form always carries growth orientation.
proof idea
Term-mode construction of the structure field base_step_grows. Unfold the normal-form composition and its level map so the goal is $M.{\rm levels}(0)\cdot\varphi^0 < M.{\rm levels}(0)\cdot\varphi^1$. Take positivity of the base from $M.{\rm levels_pos},0$ and $\varphi>1$ from PhiForcing.phi_gt_one, then close by nlinarith. No further hierarchy lemmas are needed beyond the definitions of the normal form.
why it matters
Growth orientation is one of the three legs of the canonical $\varphi$-uniform closure certificate (canonical_phi_uniform_closure), alongside uniform scale and the seed-size law. That certificate is the normal-form package used when comparing an arbitrary hierarchy to its $\varphi$-closed rewrite.
It also feeds the biconditional phiUniformClosedLevels_eq_original_iff_uniform_growth_seed: the normal form agrees with the original hierarchy exactly when the original already satisfies uniform scale, growth orientation, and seed closure. In the forcing chain this is bookkeeping for T6 ($\varphi$ forced as self-similar ratio), not a new derivation of $\varphi$ itself.
Without this lemma the closure structure cannot be inhabited for every nontrivial multilevel input, so downstream uniqueness and comparison arguments would stall at the growth field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.