realizedHierarchyMultilevelComposition
plain-language theorem explainer
From a realized hierarchy on a closed observable framework, extract the positive multilevel composition (level sizes with positivity and at least three levels). Hierarchy-forcing results cite this bridge to attach canonical uniform-scale, growth, seed-size, and base-ratio-φ laws. The body is a structure coercion: copy the level map and discharge the three positivity witnesses from the hierarchy's level positivity.
Claim. Given a closed observable framework $F$ and a realized hierarchy $H$ on $F$, the sequence of level sizes carried by $H$ forms a nontrivial multilevel composition: every level size is positive, and in particular the first three levels are positive.
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the cost foundation (Recognition Composition Law, normalization, calibration). Hierarchy structure sits between ledger/recognition forcing and the φ self-similarity step (T6).
A closed observable framework supplies a state space, dynamics, and a positive ratio observable with nontrivial range and no external moduli. A realized hierarchy on such a framework carries a sequence of positive level sizes together with the structural laws needed for multilevel composition.
Upstream, NontrivialMultilevelComposition is the HierarchyForcing interface: a level map that is everywhere positive and has at least three positive levels. The shifted cost $H(x)=J(x)+1$ and the φ-ladder appear later when those levels are forced into uniform geometric growth; this definition only packages the composition data.
proof idea
Pure structure construction. Set levels to the realized hierarchy's level map. Copy levels_pos verbatim. For at_least_three, nest two constructors and apply level positivity at indices $0$, $1$, and $2$. No external lemmas beyond the fields of the realized hierarchy.
why it matters
This is the adapter that lets every realized hierarchy enter the HierarchyForcing API. Downstream theorems attach the canonical package: uniform-scale law, growth orientation, seed-size law, and base ratio equal to φ (realizedHierarchy_canonical_base_ratio_phi, growth/seed/uniform variants). Those feed realizedHierarchy_levels_eq_phiUniform and the certificate structure RealizedHierarchyNormalFormEquivalence, which equate the realized-hierarchy route with the canonical φ-uniform normal form.
In the forcing chain this is infrastructure for T6 (φ as self-similar fixed point) and the discrete ladder that later supports T7/T8. Without the multilevel composition view, the normal-form equivalence cannot even be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.