phiLadderPosition_pos
Every position on the φ-ladder is strictly positive. Researchers working on J-cost constraints for Rogers-Ramanujan partitions cite this to confirm the entire spectrum lies in the positive reals before checking interaction costs. The proof is a one-line wrapper that invokes the standard positivity of real powers with positive base.
claimFor every integer $n$, the φ-ladder position satisfies $0 < phiLadderPosition(n)$, where $phiLadderPosition(n) := phi^n$ and $phi$ is the golden ratio.
background
The φ-ladder consists of positions $phi^n$ for $n ∈ ℤ$, introduced in this module to reinterpret the Rogers-Ramanujan 'differ by ≥ 2' rule as a J-cost admissibility condition. Adjacent occupations at $phi^n$ and $phi^{n+1}$ collapse because $phi^n + phi^{n+1} = phi^{n+2}$, so only gapped configurations minimize the interaction cost $J(phi^k)$. The upstream definition states: 'A position on the φ-ladder is $phi^n$ for integer n.'
proof idea
One-line wrapper that applies zpow_pos to phi_pos.
why it matters in Recognition Science
This positivity fact secures the discrete positive spectrum required for all subsequent J-cost calculations on the ladder, including the minimum at gap-2 occupations that recovers the Rogers-Ramanujan constraint. It sits inside the RamanujanBridge module whose doc-comment links the classical partition identities to Recognition Science via the golden recurrence and Zeckendorf representations. The result supports the broader forcing chain by guaranteeing admissible rungs before deriving T7 (eight-tick octave) and T8 (D=3) from the same φ-structure.
scope and limits
- Does not compute numerical values of any ladder position.
- Does not address J-cost or stability of multi-rung occupations.
- Does not extend to non-integer exponents.
- Does not connect directly to physical constants or forcing steps T0-T8.
formal statement (Lean)
128theorem phiLadderPosition_pos (n : ℤ) : 0 < phiLadderPosition n :=
proof body
Term-mode proof.
129 zpow_pos phi_pos n
130
131/-- Adjacent φ-ladder positions have ratio φ. -/