phiRung_pos
plain-language theorem explainer
The lemma establishes positivity of the φ-ladder scaling factor for every integer rung. Workers deriving masses or energies via the Recognition Science φ-ladder cite it to confirm all scalings stay positive. The proof reduces the claim by unfolding the definition then invokes the standard positivity result for integer powers of a positive base.
Claim. For every integer $n$, $0 < phi^n$ where $phi$ is the golden ratio and $phi^n$ denotes the scaling factor on the φ-ladder.
background
The RSNativeUnits module defines a native measurement system with tick and voxel bases, then organizes all derived quantities on the φ-ladder. The definition phiRung (n : ℤ) : ℝ := phi ^ n supplies the scaling φ^n for masses, energies, times, and lengths, as stated in the module documentation: 'RS measures are organized on a φ-ladder: φⁿ for integer n provides the natural scaling for masses, energies, times, and lengths.'
proof idea
Term-mode proof. The simp [phiRung] tactic unfolds the definition to the goal 0 < phi ^ n. The exact zpow_pos phi_pos n step then applies the upstream positivity lemma for integer powers of the positive base phi.
why it matters
The result secures the φ-ladder as a reliable scaling tool inside the Recognition Science constants layer. It directly supports the module's description of φ^n scalings and aligns with the framework's T6 fixed-point construction of phi. No downstream citations appear in the graph, yet the lemma closes a basic positivity requirement before mass or energy formulas are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.