phiLadderPosition_pos
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.