UniformClosurePreservation
plain-language theorem explainer
Packages four properties that uniform closure must satisfy on a nontrivial multilevel hierarchy: the closed form is canonically uniform-scale, levels are fixed exactly when the original was already uniform, closure is idempotent on levels, and the base ratio is unchanged. Cited by the T5→T6 self-similarity bridge and by the canonical certificate theorem. Definitional Prop bundle; uniqueness is propositional (Subsingleton).
Claim. For a nontrivial multilevel composition $M$ (positive level sequence with at least three levels), a uniform-closure preservation certificate asserts: (i) the uniform-closed normal form of $M$ obeys the canonical uniform-scale law (each adjacent step multiplies by $M$'s own base ratio); (ii) the closed levels equal the original levels for every index if and only if $M$ itself already obeys that law; (iii) closing twice leaves levels unchanged; (iv) the canonical base ratio is invariant under closure.
background
The module UnifiedForcingChain aims to force the full T0–T8 chain from the Recognition Composition Law plus normalization and calibration. The T5→T6 step needs self-similarity on a discrete ledger hierarchy: scale ratios cannot be free parameters.
A nontrivial multilevel composition is a positive real sequence of levels with at least three occupied rungs. The canonical uniform-scale law replaces a raw “no free scale” hypothesis: every adjacent step is generated by one base ratio attached to the hierarchy. Uniform closure is the normal-form operation that enforces that law while retaining the hierarchy’s identity data.
This structure does not prove those facts; it names the Prop bundle a certificate must discharge so later bridges can quote a single object rather than four separate lemmas.
proof idea
No proof body: this is a structure (definitional Prop interface). The four fields are pure specifications. A companion Subsingleton instance shows any two certificates for fixed $M$ are definitionally equal (rfl), so the certificate type is propositionally unique. The actual constructions live in canonical_uniform_closure_preservation, which fills the fields from the hierarchy lemmas on uniform-closed multilevel composition (uniform scale of the normal form, levels-equality iff already uniform, idempotence of levels, base-ratio preservation).
why it matters
Sits on the path from T5 (unique $J$, with $J(x)=(x+x^{-1})/2-1$) to T6 ($\varphi$ as the self-similar fixed point). Downstream, canonical_uniform_closure_preservation supplies the inhabited certificate for every nontrivial hierarchy, and T5_To_T6_SelfSimilarity_Bridge routes through internal hierarchy dynamics: a closed observable framework with a realized hierarchy forces the scale ratio to be $\varphi$. Packaging preservation as one certificate keeps the bridge honest about what uniform closure does and does not change (levels vs base ratio), avoiding smuggled scale freedom between uniqueness of $J$ and forcing of $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.