uniformClosedLevels_eq_original_iff_uniform_scale
plain-language theorem explainer
Uniform closure of a multilevel hierarchy leaves every level unchanged if and only if the hierarchy already obeys the canonical uniform-scale law (each adjacent step multiplies by the base ratio levels₁/levels₀). Hierarchy and forcing-chain arguments cite this biconditional as the exact-preservation criterion. Proof is a two-direction constructor: forward from the closed step relation, reverse by the existing one-way preservation lemma.
Claim. Let $M$ be a nontrivial multilevel composition (positive level sequence $\ell:\mathbb{N}\to\mathbb{R}$ with at least three positive levels). Write $\rho=\ell(1)/\ell(0)$ for its canonical base ratio, and let $\ell^{\mathrm{cl}}(k)=\ell(0)\,\rho^{k}$ be the uniform closure of the levels. Then $\ell^{\mathrm{cl}}(k)=\ell(k)$ for every $k$ if and only if $\ell(k+1)=\rho\,\ell(k)$ for every $k$.
background
In the Unified Forcing Chain, multilevel hierarchies are positive real sequences with at least three levels. The canonical base ratio of such an $M$ is $\rho=\ell(1)/\ell(0)$. The CanonicalUniformScaleLaw asserts that every adjacent step is generated by this same ratio: $\ell(k+1)=\rho,\ell(k)$. It is the theorem-shaped stand-in for a raw all-pairs no-free-scale hypothesis.
Uniform closure rebuilds the sequence geometrically from the original base level and base ratio: $\ell^{\mathrm{cl}}(k)=\ell(0),\rho^{k}$. By construction the closed sequence always steps by $\rho$ (uniformClosedLevels_step). The one-way companion already shows that if $M$ satisfies the uniform-scale law, then closure preserves every original level.
This module forces T0–T8 from the Recognition Composition Law plus normalization and calibration; hierarchy scale rigidity is part of the discreteness and ledger forcing layer that feeds self-similarity and $\varphi$.
proof idea
Term-mode constructor on the biconditional.
Forward: assume $\ell^{\mathrm{cl}}(k)=\ell(k)$ for all $k$. For each $k$, start from uniformClosedLevels_step, which gives $\ell^{\mathrm{cl}}(k+1)=\rho,\ell^{\mathrm{cl}}(k)$. Rewrite both closed levels by the preservation hypothesis to obtain $\ell(k+1)=\rho,\ell(k)$, i.e. CanonicalUniformScaleLaw.
Reverse: one-line application of the existing theorem uniformClosedLevels_eq_original_of_uniform_scale, which inducts along the geometric recurrence once the uniform-scale law is given.
why it matters
Exact preservation under uniform closure is the clean criterion that a hierarchy already carries no free scale parameters. Downstream, canonical_uniform_closure_preservation packages this biconditional as the exact_preservation_iff field of the UniformClosurePreservation certificate, together with the normal-form and idempotence facts.
In the forcing chain this sits under hierarchy and discreteness forcing: once adjacent ratios are locked to a single base ratio, self-similar fixed-point arguments (T6, $\varphi$) and the eight-tick / $D=3$ steps (T7–T8) can treat the level ladder as a pure geometric sequence rather than an arbitrary positive sequence. The result closes the gap between “closure produces a uniform object” and “the original object was already uniform.”
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.