uniformClosedLevels_step
plain-language theorem explainer
In any nontrivial multilevel composition, the uniform-closed level sequence is geometric: each successive level equals the previous times the original canonical base ratio. Hierarchy and scale-forcing arguments cite this as the inductive step of the uniform-scale law. The proof unfolds the closed-level definition and reduces via the successor power law and ring algebra.
Claim. Let $M$ be a nontrivial multilevel composition (positive real levels with at least three levels). Write $L_k$ for the uniform-closed level sequence of $M$ and $r_M$ for its canonical base ratio. Then for every $k\in\mathbb{N}$, $L_{k+1}=r_M\, L_k$.
background
The module UnifiedForcingChain assembles the complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. Hierarchy forcing sits in that chain: once free scale parameters are disallowed, adjacent level ratios must be uniform.
A nontrivial multilevel composition is a positive sequence of real levels with at least three occupied rungs. Uniform closure rebuilds that hierarchy into a pure geometric sequence whose common ratio is the original canonical base ratio (the forced adjacent-step factor extracted from $M$). The closed levels are therefore of power form, so the step relation is the discrete geometric recurrence.
Upstream, HierarchyForcing records that no free scale parameters forces uniform adjacent ratios; the present lemma is the elementary recurrence that makes that uniform-scale law hold by construction for the closed hierarchy.
proof idea
Term-mode, essentially algebraic. Introduce $k$, unfold the definition of the uniform-closed levels (a geometric sequence built from the canonical base ratio), rewrite the successor power via pow_succ, and finish by ring normalization. No external lemmas beyond the definition and the power identity are required.
why it matters
This is the inductive step that lets the uniform-closed hierarchy satisfy the canonical uniform-scale law by construction (uniformClosedMultilevelComposition_uniform_scale). That fact feeds the two comparison theorems: if the original hierarchy already obeys the uniform-scale law then closure fixes every level, and conversely levelwise equality with the original holds iff the original was already uniformly scaled.
In the forcing chain this is hierarchy bookkeeping toward self-similar discrete scale structure (the T6 φ-forcing neighborhood): once levels must step by a single base ratio, free continuous scales are eliminated and the self-similar fixed point can be forced. It does not itself derive φ; it supplies the geometric skeleton those later steps use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.