phiRung_pos
The lemma establishes that φ raised to any integer power is strictly positive. Derivations of masses, energies, and lengths on the RS φ-ladder cite this to guarantee positive values for scaled quantities. The argument is a one-line wrapper that unfolds the definition of the rung scaling and invokes the standard positivity of integer powers of a positive base.
claimFor every integer $n$, the real number $0 < r^n$ holds, where $r$ is the golden ratio and the exponentiation is the standard real power.
background
The RS-Native Measurement System module defines tick and voxel as base units, with coh and act as derived quanta, and organizes all physical measures on the φ-ladder: φ^n for integer n supplies the natural scaling for masses, energies, times, and lengths. The sibling definition phiRung computes this scaling explicitly as the real power φ^n. The upstream result in the same module states: 'φ-ladder scaling: compute φⁿ for integer rung.'
proof idea
The term proof first applies simp to unfold the definition of the rung scaling into the power expression, then invokes the lemma zpow_pos on the positivity of the golden ratio base.
why it matters in Recognition Science
The result supplies the positivity needed for the mass formula yardstick · φ^(rung - 8 + gap(Z)) and for all other ladder scalings in the constants module. It directly supports the framework landmarks that fix D = 3 and the eight-tick octave by ensuring every rung yields a positive real. No downstream uses are recorded, so the lemma functions as a basic closure property for the φ-ladder.
scope and limits
- Does not specify the numerical value of the golden ratio.
- Does not extend positivity to non-integer or real rungs.
- Does not address complex exponents or branch cuts.
- Does not supply SI conversion factors for the scaled quantities.
formal statement (Lean)
157lemma phiRung_pos (n : ℤ) : 0 < phiRung n := by
proof body
Term-mode proof.
158 simp [phiRung]
159 exact zpow_pos phi_pos n
160