Constants Rsnative Units Phi Rung Add

The phi ladder

The golden ratio phi, roughly 1.618, is the unique positive number that satisfies r² = r + 1. In the Recognition Science (RS) framework, this ratio is not just a geometric curiosity. It is the base of a scaling ladder used to set the natural sizes of physical quantities. The declaration phiRung defines this ladder: for any integer n, the value phiRung n is simply phi raised to the power n. So phiRung 0 is 1, phiRung 1 is phi itself, and phiRung (-5) is phi to the minus fifth power, which the framework identifies as the fundamental energy quantum.

The declaration phiRung_add is a theorem about how these rungs combine. It states that multiplying two rungs adds their exponents: phiRung m times phiRung n equals phiRung (m + n). This is the familiar law of exponents, applied to the golden ratio. The theorem is proved in the machine-checked library of formal theorems, meaning it is a guaranteed consequence of the definition, not an assumption. It is the algebraic backbone that lets the framework scale any measure up or down by whole powers of phi without ambiguity.

In Recognition Science, this ladder is the organizing principle for measurement. The framework's native units, such as the tick for time and the voxel for length, are defined so that the speed of light is exactly 1. All other quantities, from mass to action, are then expressed as multiples of phi to some integer power. The phiRung_add theorem ensures that these multiples compose consistently: scaling a mass by phi twice is the same as scaling it by phi squared. This consistency is what makes the unit system coherent, even though its base units are not tied to any external standard like the SI system.

The theorem does not claim that these phi-power values match any measured physical constants. The framework's definitions are choices, not measurements. For example, identifying phi to the minus fifth as the energy quantum is a definitional step, not a derived result. The theorem only governs the arithmetic of the ladder itself. It says nothing about whether the ladder's rungs correspond to real particle masses or energies; that correspondence is an empirical question the framework leaves open.

/-- φ-ladder scaling: compute φⁿ for integer rung. -/
@[simp] noncomputable def phiRung (n : ℤ) : ℝ := phi ^ n

/-- φ-ladder scaling: compute φⁿ for integer rung. -/
@[simp] noncomputable def phiRung (n : ℤ) : ℝ := phi ^ n

What this page does not claim

The theorem does not claim that any phi-power value matches a measured physical constant. The declaration does not establish that the phi ladder is the only possible scaling rule. The theorem does not prove that the framework's native units correspond to SI units.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/RSNativeUnits.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: