phiUniformClosedMultilevelComposition
plain-language theorem explainer
Packages any nontrivial multilevel hierarchy into its canonical φ-uniform closed normal form: the same structure type, with levels replaced by the φ-uniform closed level sequence. Hierarchy and forcing arguments cite it as the standard normal-form object whose base ratio is φ. The body is a structure constructor that reuses positivity of the φ-uniform levels for the three-level nontriviality witnesses.
Claim. Given any nontrivial multilevel composition $M$ (a positive real level sequence with at least three positive levels), there is an associated nontrivial multilevel composition whose levels are the $\varphi$-uniform closed levels of $M$.
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. T6 is the step that forces $\varphi$ as the self-similar fixed point of the discrete ledger.
A nontrivial multilevel composition is a map $\mathbb{N}\to\mathbb{R}$ of strictly positive level sizes with the first three levels positive. It is the raw hierarchy object on which scale-law and growth certificates act. The $\varphi$-uniform closed levels of such an $M$ are the canonical re-leveling that enforces uniform adjacent ratios at the golden ratio after seed-closure; this definition simply re-wraps that sequence as a full nontrivial multilevel composition.
Upstream, the structure only needs positivity of those $\varphi$-uniform levels (already proved as phiUniformClosedLevels_pos) so the returned object still satisfies the nontriviality package. Related canonical objects elsewhere in the foundation (arithmetic, traces, dressings) play the same role: fix a normal form so later uniqueness and ratio theorems have a single target.
proof idea
Definitional structure construction, not a deep proof. Set levels to the $\varphi$-uniform closed level sequence of $M$. Discharge levels_pos by the existing positivity lemma for that sequence. Discharge at_least_three by applying the same positivity lemma at indices $0,1,2$ inside nested constructors. No algebraic identity beyond those positivity facts is used.
why it matters
This is the normal-form carrier for $\varphi$-uniform hierarchy closure inside the forcing chain. Downstream, the base-ratio theorem states that the canonical base ratio of this object equals $\varphi$; the growth theorem installs canonical growth orientation on it; uniqueness and iff theorems characterize when the normal form agrees with the original levels (precisely when $M$ was already uniform, growing, and seed-closed).
It feeds admissible-orbit level equivalence (every admissible orbit is level-equivalent to this $\varphi$-uniform form), the admissible-orbit normal-form reflection certificate, and the closure normal-form composition package. In framework terms it is the concrete T6-facing object: once hierarchies are rewritten in this form, $\varphi$ is the forced self-similar scale, aligning with the primer landmark that $\varphi$ is the self-similar fixed point on the discrete ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.