phiRung_zero
The lemma fixes the zero rung on the φ-ladder at unity scaling. Workers normalizing reference masses or energies in the RS-native system cite it when anchoring the ladder before applying rung shifts. The result follows at once from the exponential definition of the rung function.
claimThe φ-ladder scaling function satisfies $φ^0 = 1$.
background
The RS-native unit system organizes all measures on the φ-ladder, where φ^n for integer n supplies the natural scaling for masses, energies, times, and lengths. The function phiRung is defined by phiRung(n : ℤ) := φ^n, which computes the scaling factor at rung n. This places the zero rung at the reference value 1, consistent with the base units tick and voxel where c = 1 and all dimensionless ratios derive from φ alone.
proof idea
One-line wrapper that applies the definition of phiRung via simplification.
why it matters in Recognition Science
The result anchors the φ-ladder used in mass formulas and constant derivations. It supplies the base case referenced by the number-theoretic rung function in RecognitionTheta. The zero rung is the starting point for the eight-tick octave and the derivation of D = 3 in the forcing chain.
scope and limits
- Does not define the numerical value of φ.
- Does not extend the rung function to non-integer arguments.
- Does not address the distinct natural-number rung function defined in RecognitionTheta.
formal statement (Lean)
161lemma phiRung_zero : phiRung 0 = 1 := by simp [phiRung]
proof body
162