phiRung_one
plain-language theorem explainer
Scaling by one rung on the phi-ladder multiplies any quantity by the golden ratio phi. Researchers normalizing masses or energies to the base voxel or tick in the Recognition Science unit system cite this base case. The proof reduces immediately via simplification from the power definition of the rung scaling.
Claim. Let the phi-rung scaling be defined by $f(n) := phi^n$ for integer $n$. Then $f(1) = phi$.
background
The module sets up an RS-native measurement system whose base units are the tick (one discrete ledger posting interval) and the voxel (distance light travels in one tick). Derived quanta are the coherence quantum equal to phi to the minus five and the action quantum equal to the Planck constant in these units. All dimensionless ratios are fixed by phi, and physical measures are organized on the phi-ladder as phi to the power n for integer n.
proof idea
The proof is a one-line wrapper that applies the definition of the phi-rung scaling via the simp tactic.
why it matters
This base case anchors rung-one scaling inside the RS-native constants module and thereby supports the phi-ladder used for masses, energies, and lengths. It feeds the recognition theta certificate, which records the complete additivity of the number-theoretic phi-rung together with its value at one. The result is consistent with the framework property that all dimensionless ratios are fixed by phi alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.