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

phiScale

show as:
view Lean formalization →

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.

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

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.

scope and limits

formal statement (Lean)

  69noncomputable def phiScale (n : ℤ) (x : ℝ) : ℝ := x * phi ^ n

proof body

Definition body.

  70
  71/-- φ-scaling is a group action. -/

used by (3)

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.