growthClosedLevels_pos
plain-language theorem explainer
Any nontrivial multilevel composition yields a growth-closed level sequence that remains strictly positive at every index. Hierarchy and φ-forcing arguments cite this when rebuilding a composition closed under golden-ratio growth. The proof is a short case split: at the distinguished index the value is a product of a positive level with φ>0; elsewhere it inherits positivity from the original levels.
Claim. Let $M$ be a nontrivial multilevel composition: a sequence of levels $\ell:\mathbb{N}\to\mathbb{R}$ with $\ell(k)>0$ for all $k$, and at least three positive levels. Write $\ell_M$ for the associated growth-closed level sequence (the original levels with the distinguished slot replaced by a $\varphi$-scaled product). Then $0 < \ell_M(k)$ for every $k\in\mathbb{N}$.
background
This sits in the Unified Forcing Chain module, which derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Multilevel composition is the hierarchy side of that chain: a NontrivialMultilevelComposition is a positive real sequence of levels with at least three positive entries, the raw data for scale ratios before φ is forced.
Growth-closed levels rebuild such a sequence so adjacent ratios obey the self-similar φ rule (T6 landmark: φ as the discrete-ledger fixed point). Concretely, the growth-closed sequence agrees with the original levels except at a distinguished index, where the value is a product involving φ. The structure already carries levels_pos : ∀ k, 0 < levels k, and φ-forcing supplies φ > 0.
Downstream, the canonical growth-closed multilevel composition packages this sequence as a new NontrivialMultilevelComposition, so positivity of every coordinate is a required field obligation.
proof idea
Term-mode proof by introduction on the index $k$, then unfolding the growth-closed sequence. Case split on whether $k=1$.
- If $k=1$, the unfolded value is a product of the original level at $0$ with φ. Apply
mul_postoM.levels_pos 0andPhiForcing.phi_pos. - Otherwise the value is the original level at $k$, so
M.levels_pos kfinishes it.
Both branches close by simp with the case hypothesis. No deeper hierarchy lemmas are needed; the argument is pure positivity arithmetic on the unfolded definition.
why it matters
This is the positivity witness for growthClosedMultilevelComposition, the canonical growth-closed multilevel composition built from any nontrivial $M$. That definition sets levels := growthClosedLevels M and levels_pos := growthClosedLevels_pos M, so without this theorem the rebuilt hierarchy object cannot inhabit the structure.
In the forcing chain it is scaffolding for the hierarchy step that feeds T6 (φ forced as the self-similar fixed point of the discrete ledger). Closing positivity under the φ-scaled rebuild keeps the multilevel data inside the cone where uniform adjacent-ratio theorems apply. It does not itself force φ or the eight-tick octave; it only keeps the level sequence admissible after growth closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.