phiRung_neg
plain-language theorem explainer
Scaling on the φ-ladder satisfies φ raised to a negative integer rung equals the reciprocal of the positive rung case. Researchers deriving mass or energy values from the RS-native unit system would invoke this when handling sign flips in the ladder for quantities like length or frequency. The proof reduces directly via the definition of the rung scaling and the algebraic rule for negative exponents.
Claim. For any integer $n$, the φ-ladder scaling at rung $-n$ equals the reciprocal of the scaling at rung $n$: $φ^{-n} = 1/φ^n$, where $φ$ is the golden ratio and exponentiation defines rung scaling.
background
The module sets up an RS-native unit system with tick as the atomic time quantum and voxel as the spatial step, yielding c=1 and derived quanta such as coh = φ^{-5}. The φ-ladder organizes all measures via φ^n for integer n, supplying the natural scaling for masses, energies, times, and lengths without external anchors. Upstream, the rung scaling is defined directly as φ^n, while related results fix the octave as 8 ticks and link to cycle structures in the graded ledger.
proof idea
The proof is a term-mode reduction. It first simplifies using the rung scaling definition together with the one_div property, then rewrites via the exponentiation rule for negative integers.
why it matters
This lemma secures sign symmetry on the φ-ladder, supporting bidirectional scaling in the Recognition framework and aligning with the eight-tick octave forced by D=3. It underpins mass and energy formulas that move across positive and negative rungs. No immediate downstream theorems are listed, yet the result closes a basic algebraic property required for the full native unit system.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.