pith. machine review for the scientific record. sign in
def definition def or abbrev high

scaleByPhi

show as:
view Lean formalization →

The definition multiplies a real quantity by phi to the integer power n, shifting it by n rungs on the phi-ladder. Workers in Recognition Science units apply it when rescaling masses, lengths, or energies while staying inside the tick-voxel system. It is realized as a direct multiplication by the result of phiRung.

claimFor real number $x$ and integer $n$, the scaled quantity equals $x$ times the golden ratio raised to the power $n$.

background

The RSNativeUnits module defines a native measurement system based on tick as the time quantum and voxel as the spatial quantum, with $c$ set to unity. All derived quantities such as energy and action are expressed using powers of phi, and the phi-ladder provides the scaling mechanism for masses, energies, times, and lengths. The upstream phiRung definition supplies the explicit computation of the golden ratio raised to integer $n$.

proof idea

one-line wrapper that applies phiRung

why it matters in Recognition Science

This definition belongs to the constants module and supplies the scaling primitive for the phi-ladder described in the module documentation. It supports the framework's requirement that all dimensionless ratios are fixed by phi alone. With no recorded downstream applications, it remains available for use in mass formulas and other derived quantities on the ladder.

scope and limits

formal statement (Lean)

 155@[simp] noncomputable def scaleByPhi (x : ℝ) (n : ℤ) : ℝ := x * phiRung n

proof body

Definition body.

 156

depends on (3)

Lean names referenced from this declaration's body.