uniformClosedLevels_zero
plain-language theorem explainer
Evaluating the canonically uniform-closed hierarchy at the base index recovers the original base level. Hierarchy and forcing-chain arguments cite this as the k=0 boundary condition for geometric level generation. The proof is a one-line simp unfolding of that geometric definition.
Claim. For any nontrivial multilevel composition $M$ (a positive real-valued level map $\mathbb{N}\to\mathbb{R}$ with at least three positive levels), the canonically uniform-closed level sequence of $M$ satisfies $\mathrm{level}_{\mathrm{unif}}(0)=\mathrm{level}_M(0)$.
background
The Unified Forcing Chain module derives T0–T8 as forced consequences of the cost foundation (Recognition Composition Law, normalization, calibration), from the absolute floor through logic, discreteness, ledger structure, unique $J$, $\varphi$, the eight-tick octave, and $D=3$.
A nontrivial multilevel composition packages a positive map $\mathrm{levels}:\mathbb{N}\to\mathbb{R}$ with at least three strictly positive entries. Such hierarchies model stacked discrete ledger scales. The uniform-closed construction keeps the original base level and a canonical base ratio, then generates every level geometrically: level $k$ equals base times $(\mathrm{ratio})^k$. Upstream HierarchyForcing uses that pattern to force uniform adjacent ratios when free scale parameters are disallowed.
proof idea
One-line wrapper: simp unfolds the definition of the uniform-closed level map. That definition is base times $(\mathrm{canonical\ base\ ratio})^k$; at $k=0$ the power is $1$, so the product equals the original base level. The lemma is tagged @[simp] for automatic rewriting in later hierarchy algebra.
why it matters
Local bookkeeping inside Foundation.UnifiedForcingChain: uniform closure must not move the base rung, or geometric generation would shift the whole ladder. The module's top claim is the complete inevitability chain (absolute floor through T8). This identity is not itself a T-step; it supports simp-driven reasoning about closed multilevel compositions that feed scale-forcing arguments (no free scale parameters, self-similar $\varphi$ structure at T6). No recorded downstream dependents yet; value is as a simp boundary fact rather than a named forcing theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.