canonical_uniform_closure_preservation
plain-language theorem explainer
Every nontrivial multilevel composition admits a canonical uniform-closure preservation certificate: the closed normal form obeys uniform scaling, exact level preservation is equivalent to already being uniform, closure is idempotent on levels, and the base ratio is unchanged. Cited by the T5-to-T6 self-similarity bridge in the forcing chain. Proof is a four-field structure assembly from named scale and idempotence lemmas.
Claim. Let $M$ be a nontrivial multilevel composition (positive level sizes $k\mapsto \ell_k$ with at least three levels). Then the uniform closure of $M$ satisfies: (i) the closed form obeys the canonical uniform scale law; (ii) $\forall k,\,\ell^{\mathrm{cl}}_k=\ell_k$ if and only if $M$ itself obeys that law; (iii) applying uniform closure twice leaves levels unchanged; (iv) the base adjacent ratio is preserved under closure.
background
The Unified Forcing Chain module shows T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. The T5→T6 step needs self-similarity on a discrete ledger hierarchy: once $J$ is unique, a closed multilevel scale must pin $\varphi$ as the fixed point.
A nontrivial multilevel composition is a positive map $\ell:\mathbb{N}\to\mathbb{R}$ with at least three positive levels. Uniform closure produces a normal form intended to enforce equal adjacent ratios (canonical uniform scale). The structure UniformClosurePreservation packages four Prop fields: the closed form scales uniformly; exact preservation of levels is equivalent to the original already being uniform; double closure is idempotent on levels; the base ratio is preserved.
Upstream hierarchy forcing supplies the nontrivial multilevel type and the no-free-scale principle that forces uniform adjacent ratios. This certificate is the Prop-level witness that the closure operation is well-behaved before it is fed into the T5–T6 bridge.
proof idea
Term-mode structure construction. Each of the four fields of the preservation certificate is discharged by a dedicated lemma on the same $M$:
- uniform normal form from the lemma that the uniform-closed multilevel composition obeys canonical uniform scale;
- exact-preservation equivalence from the iff relating levelwise equality after closure to the original already satisfying uniform scale;
- idempotence from the lemma that closing twice does not change levels;
- base-ratio preservation from the lemma that uniform closure keeps the base adjacent ratio.
No further tactic work: the theorem is the bundle of those four facts into one Prop certificate.
why it matters
Sits on the T5→T6 bridge of the complete inevitability chain. Downstream, t5_to_t6_bridge_holds consumes this style of closed-scale normal-form control when it asserts that internal hierarchy dynamics and realized closed scales force $\varphi$ once $J$-uniqueness (T5) is available. Without a clean preservation certificate, self-similarity on the discrete ledger would be an informal step rather than a theorem-backed bridge.
In the primer landmarks this supports T6 ($\varphi$ as the self-similar fixed point) after T5 ($J(x)=(x+x^{-1})/2-1$). The module’s stronger claim is that every level is forced, not merely compatible; packaging uniform-closure preservation is part of making the hierarchy side of that claim machine-checkable. It does not itself derive $\varphi$ or the eight-tick octave; it certifies the scale-closure hygiene those later steps rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.