canonical_closure_normal_form_composition
plain-language theorem explainer
Any nontrivial multilevel composition admits a canonical closure-composition certificate: growth, uniform, and seed closures compose to the unique φ-uniform normal form, with seed closure idempotent after the first two. Hierarchy and T5–T6 bridge arguments cite this to treat closed scale ladders as already in φ-normal form. The proof is a four-field structure term assembling four prior equality lemmas.
Claim. Let $M$ be a multilevel composition with positive level values and at least three levels. Then $M$ carries a canonical closure-composition certificate: (i) the composition of growth-closure then uniform-closure equals the direct $\varphi$-uniform normal form levelwise; (ii) applying seed-closure after that composite leaves levels unchanged; (iii) seed-then-uniform-then-growth closure equals the $\varphi$-uniform form; (iv) $M$ itself admits the full $\varphi$-uniform closure certificate (uniform scale, growth law, and seed-size law).
background
The module UnifiedForcingChain proves the complete inevitability chain T-1 through T8 from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). T5 pins the unique cost $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point of a discrete ledger hierarchy.
A nontrivial multilevel composition is a map $\mathbb{N}\to\mathbb{R}$ of strictly positive level values with at least three occupied levels. Hierarchy forcing closes such ladders under growth, uniform-ratio, and seed-size operations; the $\varphi$-uniform closed form is the normal form in which adjacent ratios are locked to $\varphi$ and the seed/growth laws hold.
ClosureNormalFormComposition packages four equalities asserting that the various closure orders agree with that $\varphi$-uniform form and that seed closure is idempotent once growth and uniform closure have run. Upstream, canonical_phi_uniform_closure already supplies the three-field $\varphi$-uniform certificate (uniform, growth, seed).
proof idea
Term-mode structure construction: each of the four fields of ClosureNormalFormComposition is filled by an existing lemma applied to $M$.
uniform_after_growth←uniformClosed_after_growthClosed_eq_phiUniformseed_after_uniform_growth_idempotent←seedClosed_after_uniformAfterGrowth_idempotent_levelsseed_uniform_growth←seedUniformGrowthClosed_eq_phiUniformfinal_phi_uniform←canonical_phi_uniform_closure
No new algebra is done here; the certificate is the bundle of those four prior results.
why it matters
This certificate is the normal-form glue between hierarchy closure operators and the T5→T6 bridge. Downstream, t5_to_t6_bridge_holds uses it under the field realized_closed_scale_normal_form_equivalence: once a realized closed scale is known to sit in the canonical composition normal form, self-similarity forces $\varphi$ (T6) from J-uniqueness (T5).
In the forcing chain, that bridge is the step from unique cost $J$ to the golden ratio as the only admissible discrete self-similar ratio. Without a proved composition certificate, the bridge would have to re-check closure orderings at each use site. The declaration therefore sits inside the Complete Inevitability Chain narrative of the module: every level forced, no free scale parameters after cost normalization and calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.