canonicalMinimalOrbitLevels_pos
plain-language theorem explainer
If the amplitude is positive and the hierarchy is minimal, every term of the canonical sequence-level orbit is strictly positive. Downstream constructions of the closed observable framework on ℕ cite this to keep all orbit levels in the positive reals. The proof unfolds the product definition and multiplies the two positivity facts.
Claim. Let $A \in \mathbb{R}$ with $A > 0$, and let $H$ be a minimal discrete hierarchy (a geometric scale ladder closed under the first non-trivial composition step). Write $\ell_k := A \cdot s_k$ for the canonical sequence-level orbit levels, where $s_k$ is the $k$-th scale of $H$. Then $\ell_k > 0$ for every $k \in \mathbb{N}$.
background
The module UnifiedForcingChain assembles the complete inevitability chain from the cost foundation (Recognition Composition Law plus normalization and calibration) through T-1 to T8: absolute floor, logic, MP, discreteness, ledger, recognition, unique J, φ, the eight-tick octave, and D = 3.
A MinimalHierarchy is a geometric scale ladder closed under the first non-trivial composition step; its scales form a GeometricScaleSequence whose positivity is already recorded (scale_pos: each scale is a positive power of φ). The canonical sequence-level orbit is the pointwise product of a fixed real amplitude with those scales: $\ell_k = A \cdot s_k$. That sequence is the realizable target orbit; embedding it into a closed observable framework is a separate finite-description step.
Positivity of every level is the elementary arithmetic precondition for treating the orbit as a positive real-valued observable sequence on the countable state space ℕ.
proof idea
Term-mode, three steps. Introduce the level index $k$. Unfold the definition of the canonical orbit levels to the product $A \cdot s_k$. Apply real multiplication-positivity to the two hypotheses $A > 0$ and $s_k > 0$ (the latter from scale_pos on the hierarchy's scale sequence). No further structure of minimality or closure is used.
why it matters
Feeds canonicalMinimalOrbitFramework, which builds the canonical closed observable framework carrying the minimal orbit on state space ℕ and requires a positive amplitude together with this levelwise positivity. Inside the forcing chain, that framework is the concrete countable realization of the discrete hierarchy forced by cost (T2 discreteness, T6 φ-ladder scales). Without levelwise positivity the orbit could not serve as a positive observable sequence in the closed-framework interface. The result is pure arithmetic bookkeeping; the substantive forcing work lives upstream in hierarchy minimality and scale positivity, and downstream in the framework packaging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.