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

mass_rung

show as:
view Lean formalization →

The definition assigns the mass-energy at integer rung n on the phi-ladder by scaling the sector yardstick by phi to the power n. Modelers of the Recognition Science mass hierarchy cite it when deriving rung ratios or separation properties from the forced phi fixed point. The definition is a direct algebraic expression using real exponentiation with no auxiliary lemmas.

claimThe mass-energy at rung $n$ on the phi-ladder is $m(n) = A phi^n$, where $A$ is the sector yardstick.

background

In the Spectral Emergence module the phi-ladder realizes the mass hierarchy forced by T6 (phi as self-similar fixed point) and T7 (eight-tick octave). The yardstick $A$ is taken from the Anchor definition $A_s = 2^{B_{pow}} E_{coh} phi^{r_0}$ for each sector $s$. This supplies the explicit scaling $m(n) = A phi^n$ that implements J-cost on phi-ratio edges within the Q3 structure derived from D=3.

proof idea

One-line definition that multiplies the yardstick by phi raised to the real power corresponding to the integer rung n, relying only on the built-in real exponentiation operation.

why it matters in Recognition Science

This definition supplies the explicit mass formula used by the downstream theorems mass_rung_pos, mass_rung_step, rung_ratio, rung_separation and SpectralEmergenceCert in the same module. It fills the phi-ladder mass hierarchy entry in the module documentation, which traces back to T6 (phi forced) and the Recognition Composition Law. The parent chain runs from T8 (D=3) through the Q3 automorphism group to the full spectral emergence certificate.

scope and limits

formal statement (Lean)

 284def mass_rung (yardstick : ℝ) (n : ℤ) : ℝ :=

proof body

Definition body.

 285  yardstick * phi ^ (n : ℝ)
 286
 287/-- **THEOREM**: Moving up one rung scales mass by φ. -/

used by (5)

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

depends on (11)

Lean names referenced from this declaration's body.