growthClosedMultilevelComposition_growth
plain-language theorem explainer
Any nontrivial multilevel composition, after growth-closure, carries canonical growth orientation: level 1 strictly exceeds level 0. Used when packaging growth-closure preservation in the unified forcing chain. Proof unfolds the closed levels, invokes base positivity and φ > 1, and finishes by nonlinear arithmetic.
Claim. Let $M$ be a nontrivial multilevel composition (a positive real sequence of levels with at least three positive entries). The growth-closed hierarchy built from $M$ has canonical growth orientation: its level at index $0$ is strictly less than its level at index $1$.
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. Hierarchy data enter as NontrivialMultilevelComposition: a map $\mathbb{N}\to\mathbb{R}$ of strictly positive levels with at least three positive entries.
Canonical growth orientation is the order-level stand-in for a divided ratio greater than one: it asserts only that the first step grows, $M.{\rm levels},0 < M.{\rm levels},1$. Growth-closure rebuilds a hierarchy whose adjacent steps are forced by the self-similar scale $\varphi$ (T6), via the auxiliary level function growthClosedLevels.
Upstream, $\varphi>1$ is already forced in PhiForcing; positivity of every original level is part of the multilevel structure. Those two facts are the only numerical inputs needed for the base step of the closed hierarchy.
proof idea
Term-mode structure instance whose sole field base_step_grows is proved by tactics. Rewrite the goal as growthClosedLevels M 0 < growthClosedLevels M 1, then simp with the definition of growthClosedLevels. Pull M.levels_pos 0 (base level positive) and PhiForcing.phi_gt_one. Close the resulting strict inequality by nlinarith. No separate lemmas beyond those two facts.
why it matters
Supplies the growth_normal_form field of canonical_growth_closure_preservation, the certificate that growth-closure preserves the hierarchy while normalizing the base ratio to $\varphi$ and characterizing exact preservation by a pure $\varphi$-step. That certificate sits inside the T6 leg of the forcing chain: self-similarity in the discrete ledger forces $\varphi$ as the unique growth scale. Without this orientation fact, the closed hierarchy would not be known to point "upward" at the first rung, and the later base-ratio and exact-preservation clauses could not be assembled into a single preservation package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.