uniformClosedLevels_pos
plain-language theorem explainer
The uniform-closed level sequence attached to any nontrivial multilevel composition is strictly positive at every index. Hierarchy and scale-forcing arguments that replace an arbitrary positive level tower by its constant-ratio closure cite this fact. The proof unfolds the geometric definition and multiplies base-level positivity by a positive power of the first adjacent ratio.
Claim. Let $M$ be a nontrivial multilevel composition: a map $\ell:\mathbb{N}\to\mathbb{R}$ with $\ell(k)>0$ for all $k$, and with the first three values positive. Write $\ell^{\mathrm{uc}}_M$ for the uniform-closed level sequence built from $M$ (geometric sequence with base $\ell(0)$ and common ratio $\ell(1)/\ell(0)$). Then for every $k\in\mathbb{N}$, $0 < \ell^{\mathrm{uc}}_M(k)$.
background
The ambient module is the Unified Forcing Chain: it derives the full T-1 through T8 stack as inevitabilities from the Recognition Composition Law plus normalization and calibration, rather than as mere compatibility constraints.
A nontrivial multilevel composition is a positive real sequence of levels with at least three strictly positive entries. It is the raw hierarchy data before any scale-fixing. The uniform-closed level sequence rebuilds that data as a pure geometric progression whose first term is the base level and whose common ratio is the first adjacent ratio. That construction is the concrete carrier of the slogan that free scale parameters are forbidden: once adjacent ratios are forced equal, the whole tower is determined by two positive numbers.
Positivity of the rebuilt sequence is not automatic from the type alone; it must be discharged so the rebuilt object still inhabits the nontrivial multilevel composition structure (which demands a positive level map).
proof idea
Term-mode proof after a single intro k. Unfold the uniform-closed levels definition to the product of the base level with the $k$-th power of the first adjacent ratio. Apply real multiplication positivity to that product: the base factor is positive by the multilevel composition's level-positivity at index 0; the power factor is positive by power-positivity of a positive real, whose base is the quotient of level 1 by level 0, itself positive by division-positivity of two positive reals. No hierarchy-specific lemmas beyond the structure's positivity field are required.
why it matters
This lemma is the positivity witness consumed by the canonical uniform-closed multilevel composition constructor in the same module: that definition sets levels to the uniform-closed sequence and plugs this theorem in as levels_pos. Without it the rebuilt hierarchy would not type-check as a nontrivial multilevel composition.
In the forcing narrative, uniform closure is the step that eliminates free scale parameters in multilevel cost hierarchies. It sits upstream of the discrete self-similarity that forces $\varphi$ (T6) and of the octave/dimension package (T7–T8). The parent definition packages a cleaned hierarchy ready for those later forcing steps; this positivity fact is the small arithmetic hinge that keeps the package inside the structure's hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.