growthClosedLevels_eq_original_iff_phi_step
plain-language theorem explainer
Growth closure leaves a multilevel hierarchy unchanged if and only if its first adjacent step is already the canonical φ-step. Hierarchy and φ-forcing arguments cite this as the exact fixed-point criterion for the growth-closed normal form. The proof is a short biconditional: evaluate at level 1 one way, and case-split on k=1 versus the non-one preservation lemma the other way.
Claim. Let $M$ be a nontrivial multilevel composition (positive real levels with at least three occupied rungs). Write $M'$ for the growth-closed copy of $M$, which replaces level $1$ by $M_0\cdot\varphi$ and leaves every other level fixed. Then $M'_k=M_k$ for all $k$ if and only if $M_1=M_0\cdot\varphi$.
background
In the Unified Forcing Chain, T0–T8 are derived as inevitabilities from the Recognition Composition Law plus normalization and calibration. Around T6, discrete self-similarity forces the golden ratio $\varphi$ as the unique admissible growth factor on a ledger hierarchy.
A nontrivial multilevel composition is a map $\mathbb{N}\to\mathbb{R}$ of strictly positive levels with at least three occupied rungs. Growth closure canonically reorients such a hierarchy: it sets the first step to the $\varphi$-step above the base and copies every other level unchanged. The resulting object is again a nontrivial multilevel composition.
The companion fact that growth closure preserves every non-level-1 entry isolates the only possible discrepancy between $M$ and its closed form to the adjacent ratio at the base.
proof idea
Prove the biconditional by constructor.
Forward: from universal equality of levels, specialize at $k=1$. Unfolding the definition of growth-closed levels yields $M_0\cdot\varphi=M_1$ after symmetry.
Reverse: assume $M_1=M_0\cdot\varphi$. For arbitrary $k$, case on $k=1$. The equal case reduces to the same unfolding and the hypothesis. The unequal case is exactly the already-proved preservation lemma for non-level-1 entries of the growth-closed composition.
why it matters
This is the exact-preservation half of the canonical growth-closure certificate. Downstream, canonical_growth_closure_preservation packages growth normal form, base ratio, and this iff as the preservation certificate for any nontrivial multilevel composition. The idempotence theorem for applying growth closure twice also sits on the same scaffolding: once the first step is the $\varphi$-step, a second pass changes nothing.
In the forcing chain this pins the T6 self-similarity step: hierarchies that are already growth-closed are precisely those whose base adjacent ratio is $\varphi$, matching the unique fixed point forced by discrete ledger self-similarity. It does not itself derive $\varphi$ from the cost law; it characterizes when the canonical $\varphi$-reorientation is a no-op.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.