growthClosedLevels_one
plain-language theorem explainer
Evaluating the growth-closed reorientation of a multilevel hierarchy at step 1 yields exactly the base level times φ. Hierarchy and φ-forcing arguments cite this as the canonical first-step identity. The proof is a one-line simp unfolding of the piecewise definition.
Claim. Let $M$ be a nontrivial multilevel composition (positive real levels, at least three occupied). Write $L$ for its level sequence and $L'$ for the growth-closed reorientation that forces the first step to be the $\varphi$-step above the base. Then $L'(1) = L(0)\cdot\varphi$.
background
The module UnifiedForcingChain aims to derive the full T0–T8 chain as inevitabilities from the Recognition Composition Law plus normalization and calibration. T6 in that chain is the forcing of the golden ratio $\varphi$ as the self-similar fixed point of discrete ledger scaling.
A NontrivialMultilevelComposition is a hierarchy with a positive real level sequence $L:\mathbb{N}\to\mathbb{R}_{>0}$ that occupies at least the first three rungs. The companion definition growthClosedLevels canonically reorients such a hierarchy: it replaces level 1 by $L(0)\cdot\varphi$ and leaves every other level unchanged. That is the minimal move that installs a $\varphi$-step immediately above the base while preserving the rest of the data.
This simp lemma records the evaluation of that reorientation at index 1, so downstream hierarchy arguments can rewrite the first step without unfolding the piecewise definition by hand.
proof idea
One-line wrapper. Unfold growthClosedLevels by simp; the branch $k=1$ is definitionally $M.\mathrm{levels},0\cdot\varphi$, which is the goal.
why it matters
In the forcing chain, T6 asserts that $\varphi$ is forced as the self-similar scale of a discrete ledger. Growth-closed reorientation is the local device that installs that $\varphi$-step on an arbitrary multilevel hierarchy without inventing free scale parameters. This identity is the atomic rewrite for the first rung of that construction.
No downstream consumers are recorded yet in the dependency graph, so the lemma presently serves as a simp-facing API fact inside UnifiedForcingChain rather than a load-bearing step of a named parent theorem. It still belongs in the foundation layer: without a clean first-step identity, later claims that a hierarchy is growth-closed at the $\varphi$ ratio become notationally noisy. Framework landmark: T6 ($\varphi$ forced).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.