phiRung_neg_one
plain-language theorem explainer
The lemma states that the phi-ladder scaling function at rung negative one equals the reciprocal of phi. Researchers normalizing RS-native masses, energies, or coherence quanta on the phi-ladder cite this identity for inverse scalings. The proof is a one-line simp wrapper that unfolds the definition phiRung n = phi^n and reduces the negative exponent.
Claim. Let $phi$ denote the golden ratio. The phi-ladder scaling function satisfies $phiRung(-1) = 1/phi$ where $phiRung(n) := phi^n$ for integer $n$.
background
The RSNativeUnits module sets up a recognition-science unit system with tick and voxel as base standards and organizes all derived quantities on the phi-ladder, where phi^n for integer n supplies the natural scaling for masses, energies, times, and lengths. The upstream definition phiRung (n : Z) : R := phi ^ n computes this scaling explicitly and carries the simp attribute. The lemma supplies the concrete value at rung -1, which appears in contexts such as coherence quanta (phi^-5) and negative-rung normalizations.
proof idea
One-line wrapper that applies simp to the definition of phiRung together with the rules zpow_neg_one and one_div.
why it matters
The identity closes the negative-rung case on the phi-ladder inside the RS-native constants module and supports mass and energy formulas that invoke phi^(rung - 8 + gap(Z)). It aligns with the framework landmarks T5 (J-uniqueness) and T6 (phi as self-similar fixed point) by making inverse scalings explicit. No direct downstream theorems are recorded, yet the result is a prerequisite for any calculation that crosses from positive to negative rungs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.