growthClosedLevels_zero
plain-language theorem explainer
The growth-closed reorientation of a multilevel hierarchy leaves the base level untouched: at index 0 the reoriented sequence equals the original base value. Hierarchy and φ-forcing arguments cite this as the base-case simp fact. The proof is a one-line unfolding of the piecewise definition.
Claim. Let $M$ be a nontrivial multilevel composition (positive real levels with at least three occupied rungs). Write $L_k$ for its level sequence. The growth-closed reorientation $\widetilde{L}$ satisfies $\widetilde{L}_0 = L_0$.
background
The module UnifiedForcingChain assembles the complete inevitability chain T-1 through T8 from the Recognition Composition Law, normalization, and calibration. Within that chain, multilevel hierarchies appear when discrete ledger structure forces self-similar scale ratios (the T6 φ step).
A NontrivialMultilevelComposition is a map $\mathbb{N}\to\mathbb{R}$ of strictly positive levels with the first three rungs occupied. The auxiliary growthClosedLevels canonically reorients such a hierarchy: it replaces the first step by the φ-multiple of the base level and leaves every other index alone. Explicitly, $\widetilde{L}(k)=L_0\cdot\varphi$ when $k=1$, and $\widetilde{L}(k)=L_k$ otherwise.
This lemma records the $k=0$ case of that piecewise definition, which is needed whenever one reasons about the base rung after growth-closure.
proof idea
One-line simp wrapper. Unfolding growthClosedLevels exposes the conditional if k = 1 then ... else M.levels k. At $k=0$ the guard fails, so the else branch returns M.levels 0 definitionally.
why it matters
Growth-closure is the bookkeeping step that forces the first adjacent ratio of a multilevel hierarchy to be exactly φ, matching the self-similar fixed point of T6 in the forcing chain. The zero-index identity anchors that construction: the base rung is an invariant of the reorientation, so subsequent ratio and closedness arguments can quote the original floor without renormalizing it.
No downstream theorems currently depend on this simp fact in the graph, but it is the natural base case beside the $k=1$ φ-step clause. It sits inside Foundation.UnifiedForcingChain alongside the absolute-floor and T0–T8 package, where discrete ledger self-similarity is derived rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.