pith. machine review for the scientific record. sign in
lemma other other high

phiRung_one

show as:
view Lean formalization →

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.

claimLet 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 163lemma phiRung_one : phiRung 1 = phi := by simp [phiRung]

proof body

 164

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.