uniformClosedMultilevelComposition
plain-language theorem explainer
Canonical uniform-closed multilevel composition: replace any nontrivial hierarchy by the geometric sequence with the same base level and base ratio. Hierarchy and φ-forcing arguments cite it as the normal form that erases free scale parameters while keeping the base ratio. The construction packages uniformClosedLevels with positivity and the three-level witness.
Claim. Given a multilevel composition $M$ (a positive real sequence with at least three positive levels), form the uniform-closed composition whose level-$k$ value is $\mathrm{levels}_M(0)\cdot r_M^k$, where $r_M$ is the canonical base ratio of $M$. The resulting sequence is again a nontrivial multilevel composition.
background
The Unified Forcing Chain module shows T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Inside that chain, hierarchies of positive scales appear when self-similarity and discrete ledger structure force a geometric ladder (the T6 φ step).
A nontrivial multilevel composition is a map $\mathbb{N}\to\mathbb{R}$ with every level strictly positive and the first three levels positive. Uniform closure keeps the original base level and canonical base ratio, then rebuilds every level geometrically: $\mathrm{uniformClosedLevels}(M)(k)=M.\mathrm{levels}(0)\cdot(\mathrm{canonicalBaseRatio},M)^k$. That erases free adjacent-scale parameters while preserving the base ratio that later theorems identify with $\varphi$.
Positivity of the closed sequence is already proved as uniformClosedLevels_pos; the present definition only packages that sequence back into the multilevel-composition structure.
proof idea
Structure construction, not a deep proof. Set levels to uniformClosedLevels M. Discharge levels_pos by the existing positivity theorem for that sequence. For at_least_three, apply positivity at indices $0,1,2$ and pack the three conjuncts with nested constructors.
why it matters
This is the canonical uniform-closed normal form used throughout the hierarchy-forcing half of the chain. Downstream, seed-size laws on the uniform-closed object force the original base ratio to equal $\varphi$ (canonicalBaseRatio_eq_phi_of_uniformClosed_seed). Growth-then-uniform closure is shown equal to the direct $\varphi$-uniform form, and further seed closure is idempotent on levels (uniformClosed_after_growthClosed_eq_phiUniform, seedUniformGrowthClosed_eq_phiUniform, seedClosed_after_uniformAfterGrowth_idempotent_levels). The ClosureNormalFormComposition certificate is stated in terms of this object.
In framework terms it sits under T6 (φ forced as the self-similar fixed point of the discrete ledger): uniform closure is the map that turns an arbitrary positive hierarchy into the geometric ladder whose only free ratio is later pinned to $\varphi$. It does not itself prove φ; it supplies the normal form those pinning theorems act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.