phiScale_neg
plain-language theorem explainer
The scaling map on the φ-ladder is invertible for integer rung shifts: applying a shift by n followed by a shift by -n recovers the original real value. A researcher checking consistency of mass or timescale hierarchies under the Recognition φ-ladder hypothesis would cite this to confirm that the integer group acts freely. The proof is a one-line term rewrite that invokes additivity of the scaling exponent, negation cancellation in the integers, and the zero-shift identity.
Claim. Let $s(n,x)$ denote the map that scales the real number $x$ by the $n$th power of the golden ratio. Then $s(-n,s(n,x))=x$ for every integer $n$ and every real $x$.
background
The φ-ladder hypothesis states that privileged physical scales take the form $X=X_0·φ^n$ for integer $n$, treated here as an explicit hypothesis that generates empirical obligations rather than a definitional truth. The scaling map $s$ satisfies additivity in the exponent (sibling result phiScale_add) and the identity $s(0,x)=x$ (sibling result phiScale_zero). The module RRF.Hypotheses.PhiLadder supplies the local setting in which these algebraic properties are recorded before any physical interpretation is imposed.
proof idea
The proof is a term-mode one-liner. It rewrites the left-hand side by the additivity property of the scaling map, cancels the integer pair $n+(-n)$, and reduces the resulting zero-shift case to the identity map.
why it matters
The result supplies the inverse property required for the integer shifts to form a group action on the ladder, directly supporting the PhiLadderHypothesis class that encodes the full hypothesis. It aligns with the self-similar fixed point (T6) and the eight-tick octave structure of the forcing chain by guaranteeing that rung displacements remain closed under negation. No downstream use sites are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.