growthClosedLevels_preserves_non_one
plain-language theorem explainer
Growth closure of a nontrivial multilevel hierarchy leaves every level except index 1 unchanged. Hierarchy and φ-forcing arguments cite this to isolate the single free slot where the self-similar step can act. The proof is a one-line simplification against the definitions of growth-closed levels and multilevel composition.
Claim. Let $M$ be a nontrivial multilevel composition (a positive real level function with at least three occupied levels). For every index $k \neq 1$, the growth-closed multilevel composition built from $M$ has the same $k$-th level as $M$.
background
The module UnifiedForcingChain derives the full T0–T8 inevitability ladder from the Recognition Composition Law plus normalization and calibration. Near T6, discrete self-similarity forces the golden ratio $\varphi$ as the unique admissible growth factor on a multilevel ledger.
A NontrivialMultilevelComposition is a map $\mathrm{levels}:\mathbb{N}\to\mathbb{R}$ with every value positive and with levels $0,1,2$ strictly positive, so at least three scales are present. Growth closure rebuilds such a hierarchy so that adjacent ratios become compatible with canonical self-similar growth; by construction that rebuild is allowed to touch only the first step (level index $1$).
This lemma records the complementary fact: every non-$1$ entry is copied verbatim. Downstream comparison of the closed hierarchy with the original one can therefore reduce to a single equality at level $1$.
proof idea
Term-mode proof by introduction of $k$ and $k\neq 1$, then simp on the definitions of the growth-closed multilevel composition and of growth-closed levels, discharging with the inequality hypothesis. No external lemmas are needed beyond those definitional unfoldings: the $k\neq 1$ branch of growthClosedLevels is definitionally the original level.
why it matters
Feeds directly into growthClosedLevels_eq_original_iff_phi_step, which states that growth closure fixes the whole hierarchy if and only if the original first step already equals the canonical $\varphi$-step $M.0\cdot\varphi$. Isolating the non-$1$ levels makes that biconditional a pure statement about level $1$.
In the forcing chain this sits at the T6 gate: $\varphi$ is forced as the self-similar fixed point of discrete ledger growth. Without a clean preservation lemma, one could not separate “already $\varphi$-closed” hierarchies from those that still need the growth adjustment. The result is local bookkeeping inside Foundation, not a new physical constant, but it is the hinge that lets the $\varphi$-step characterization go through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.