phiRung_neg
phiRung_neg records the reciprocity phi^{-n} = 1/phi^n for integer rung n on the Recognition Science phi-ladder. Workers deriving mass or energy values from the yardstick formula would invoke it to flip between positive and negative tiers without separate cases. The proof is a two-line term reduction that unfolds the definition of phiRung and applies the standard negative-exponent rule for real powers.
claimFor every integer $n$, the phi-ladder scaling satisfies $phi^{-n} = 1/phi^n$.
background
The module RSNativeUnits equips Recognition Science with a native measurement system whose base units are the tick (one ledger interval) and voxel (light travel distance in one tick). All derived quantities sit on the phi-ladder: phi^n for integer n supplies the natural scaling for masses, energies, lengths and times, with c fixed to 1. The sibling definition phiRung (n : Z) := phi ^ n makes this scaling explicit and simp-friendly. Upstream results supply the octave period (8 ticks) and the graded ledger cycle structure that together force the discrete rung structure used here.
proof idea
The term proof first applies simp only [phiRung, one_div] to replace both sides by the corresponding real powers, then rewrites with zpow_neg to obtain the reciprocal. No additional lemmas or case splits are required.
why it matters in Recognition Science
The lemma supplies the group-inverse property required for the phi-ladder to act as a consistent scaling group inside the RS-native units. It directly supports the mass formula (yardstick times phi to a rung offset) and the alpha-band calculations that appear in sibling constants. While used_by count is currently zero, the reciprocity is presupposed by any downstream derivation that inverts a rung, such as negative-energy or conjugate-tick constructions. It closes a basic algebraic gap left open by the definition of phiRung itself.
scope and limits
- Does not establish existence or algebraic properties of phi.
- Does not extend the relation to non-integer rungs.
- Does not derive any physical unit conversion factors.
- Does not reference the 8-tick octave or J-cost beyond the shared module context.
formal statement (Lean)
172lemma phiRung_neg (n : ℤ) : phiRung (-n) = 1 / phiRung n := by
proof body
Term-mode proof.
173 simp only [phiRung, one_div]
174 rw [zpow_neg]
175
176/-! ## The 8-Tick Cycle
177
178The fundamental ledger cycle has period 8 = 2³ (forced by D=3).
179This defines the octave structure of RS.
180-/
181
182/-- The octave period: 8 ticks. -/