uniformClosedLevels_one
plain-language theorem explainer
For any nontrivial multilevel composition, the canonically uniform-closed level sequence agrees with the original hierarchy at index 1. Hierarchy and forcing arguments cite this as a simp fact that the geometric closure preserves the first rung. The proof unfolds the geometric definition and cancels the base ratio by field simplification.
Claim. Let $M$ be a multilevel composition with positive levels $L:\mathbb{N}\to\mathbb{R}$ and at least three positive rungs. Write $r=L(1)/L(0)$ for the base ratio and define the uniform-closed sequence by $\widetilde{L}(k)=L(0)\,r^{k}$. Then $\widetilde{L}(1)=L(1)$.
background
The module UnifiedForcingChain aims to force the full T-1 through T8 chain from the Recognition Composition Law plus normalization and calibration. Multilevel hierarchies appear when discrete ledger scales stack; a NontrivialMultilevelComposition is a positive real sequence of levels with at least three positive rungs.
The base ratio of such an $M$ is $L(1)/L(0)$. Uniform closure rebuilds every level geometrically from the original base level and that ratio: $\widetilde{L}(k)=L(0),(L(1)/L(0))^{k}$. This is the theorem-shaped stand-in for a hierarchy with no free adjacent scale parameters.
The present lemma is the $k=1$ normalization check for that construction: the closed sequence must recover the original first rung, so the geometric law is a genuine closure rather than a rescaling of the base step.
proof idea
One-line algebraic simplification. Unfold uniformClosedLevels and canonicalBaseRatio to obtain $L(0)\cdot(L(1)/L(0))^{1}$. Then field_simp cancels the nonzero denominator $L(0)$, using positivity of level 0 from the multilevel structure. The result is definitional equality with $L(1)$.
why it matters
Uniform closure is the bridge from an arbitrary positive multilevel hierarchy to a pure geometric ladder with a single free base ratio. Preserving level 1 is the minimal sanity condition for that bridge: without it, the closed sequence would not be a faithful reparametrization of the original first step.
In the forcing chain this supports the self-similar discrete ledger picture behind T6 ($\varphi$ as the unique self-similar fixed point) and the subsequent octave and dimension steps (T7 eight-tick, T8 $D=3$). No downstream consumers are recorded yet; the lemma is marked @[simp] so later hierarchy identities can discharge the $k=1$ case automatically.
It does not itself force $\varphi$ or discreteness; it only locks the geometric closure at the first rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.