phiUniformClosedLevels_pos
plain-language theorem explainer
The φ-uniform closed level sequence of any nontrivial multilevel composition is strictly positive at every index. Hierarchy and self-similarity arguments cite this when packaging a φ-scaled ladder as a valid multilevel composition. The proof unfolds the geometric definition and multiplies base-level positivity by φ^k > 0.
Claim. Let $M$ be a nontrivial multilevel composition: a sequence of positive reals with at least three positive levels. Write $\ell_M^\varphi$ for the associated $\varphi$-uniform closed level sequence (base level times successive powers of $\varphi$). Then $\forall k\in\mathbb{N}$, $0 < \ell_M^\varphi(k)$.
background
The module UnifiedForcingChain derives the full T-1 through T8 chain from the Recognition Composition Law plus normalization and calibration. T6 forces φ as the self-similar fixed point of the discrete ledger; multilevel compositions are the bookkeeping objects for that self-similarity.
A NontrivialMultilevelComposition is a sequence levels : ℕ → ℝ that is strictly positive at every index and has at least three positive levels. The φ-uniform closed levels rebuild such a sequence by fixing the base level and scaling by successive powers of φ (the unique positive solution of $x = 1 + 1/x$).
Positivity of φ itself is already available from PhiForcing. The present lemma only has to transfer that positivity, together with positivity of the base level, onto every rung of the rebuilt ladder.
proof idea
Term-mode after a single intro k. Unfold the definition of the φ-uniform closed levels (base level times φ^k). Apply real multiplication positivity to the product of two facts: the base level is positive by the multilevel composition's levels_pos at 0, and φ^k is positive by pow_pos from PhiForcing.phi_pos. No further case splits.
why it matters
This is the positivity witness required by the structure fields of phiUniformClosedMultilevelComposition, the canonical φ-uniform multilevel composition attached to any hierarchy. That constructor is the bridge from an arbitrary nontrivial multilevel composition to one whose adjacent ratios are locked to φ.
In the forcing chain this sits under T6 (φ forced as the self-similar fixed point) and supports the hierarchy side of the complete inevitability argument: once levels are φ-uniform and positive, the no-free-scale theorem of HierarchyForcing can fire. It does not itself prove uniqueness of J or the eight-tick octave; those are T5 and T7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.