phiScale
plain-language theorem explainer
The scaling operation multiplies a real number by an integer power of the golden ratio. Researchers deriving mass ladders or timescale hierarchies from the φ-ladder hypothesis cite this construction when expressing privileged scales. It is supplied directly as a definition that implements the multiplication without further obligations.
Claim. The scaling of a real number $x$ by the $n$th power of the golden ratio is given by $x · φ^n$ for integer $n$.
background
The module states that the φ-ladder hypothesis organizes privileged physical scales as $X = X_0 · φ^n$ for integer $n$, with examples including particle masses and timescales. This definition supplies the explicit scaling map that realizes the hypothesis. Upstream results supply algebraic tautologies from edge-length constructions and structure definitions from mechanism design and mock theta constructions that anchor the combinatorial setting.
proof idea
The declaration is introduced as a direct definition using real multiplication and integer exponentiation. No lemmas or tactics are applied.
why it matters
The definition is invoked by the additivity theorem for scaling, the negation theorem, and the zero theorem to establish a group action. It supplies the scaling component of the explicit φ-ladder hypothesis, which generates testable predictions and connects to the self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.