growthClosedLevels
plain-language theorem explainer
Given any nontrivial multilevel hierarchy, this builds the canonically oriented level sequence that forces the first adjacent step to be multiplication by φ while leaving every other level untouched. Hierarchy and φ-forcing arguments cite it when they need a growth-closed representative without changing the rest of the ladder. The body is a one-line piecewise definition.
Claim. For a nontrivial multilevel composition $M$ (positive real levels with at least three occupied rungs), define the growth-closed level map $L_M^{\mathrm{gc}}:\mathbb{N}\to\mathbb{R}$ by $L_M^{\mathrm{gc}}(1)=M.\mathrm{levels}(0)\cdot\varphi$ and $L_M^{\mathrm{gc}}(k)=M.\mathrm{levels}(k)$ for all $k\neq 1$.
background
The ambient module is the Unified Forcing Chain: T-1 through T8 are derived as inevitabilities from the Recognition Composition Law plus normalization and calibration. T6 is the step that forces φ as the self-similar fixed point of the discrete ledger.
Upstream, a nontrivial multilevel composition is a structure with a level map $\mathbb{N}\to\mathbb{R}$, strict positivity at every index, and at least three positive base rungs (levels 0, 1, 2). Adjacent ratios of such hierarchies are the raw material for scale-free growth arguments in HierarchyForcing.
φ here is the golden-ratio fixed point already forced in the PhiForcing layer. Growth closure is the bookkeeping move that orients the first step of an arbitrary hierarchy onto that φ-step so later lemmas can talk about a single canonical representative.
proof idea
Definitional, not a proof. The map is the piecewise function that replaces index 1 by base-level times φ and returns the original level at every other index. Downstream simp lemmas (growthClosedLevels_zero, growthClosedLevels_one) discharge the two cases by unfolding.
why it matters
This is the level-sequence kernel of the canonical growth-closed multilevel composition, which packages the same levels with positivity and the three-rung witness. Downstream facts record that the construction is positive, fixes level 0, forces level 1 to the φ-step, and leaves every non-1 entry unchanged.
The equality criterion growthClosedLevels_eq_original_iff_phi_step then says the closed hierarchy agrees with the original exactly when the original first step was already the φ-step. That is the local bridge into T6-style self-similarity: once hierarchies are growth-closed, uniform adjacent ratios and φ-forcing arguments apply without free scale parameters at the first rung.
It does not itself prove φ uniqueness; it supplies the oriented ladder those proofs consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.