Physicists modeling ultramassive black holes cite the φ-rung to decompose any positive mass M as M₀ φ^r on the self-similar ladder. The definition recovers the exact real exponent r such that M equals M₀ times φ to the power r. It is introduced as a direct definition using the change-of-base logarithm to support scaling relations for black-hole entropy and temperature in the Recognition framework.
claimThe rung $r$ for mass $M$ relative to reference mass $M_0$ is $r = log_φ(M/M_0) = ln(M/M_0)/ln φ$, where $M, M_0 > 0$.
background
In the Recognition Science treatment of ultramassive black holes, masses are placed on the φ-ladder where each step multiplies by φ, the self-similar fixed point from the forcing chain. The integer rung function in Constants.RSNativeUnits computes φ^n for n ∈ ℤ. This real-valued extension computes the continuous exponent for arbitrary positive masses, as stated in the module doc-comment: every positive mass has a unique decomposition M = M₀ · φ^r for some reference mass M₀ and rung r ∈ ℝ. The local setting is the formalization of the no-singularity theorem, RS entropy S_BH = (ln φ) · A/(4ℓ₀²), and Hawking temperature for objects like TON 618.
proof idea
The definition is a direct one-line expression: Real.log (M / M₀) / Real.log phi. This is the change-of-base formula that solves φ^r = M/M₀ for the real exponent r.
why it matters in Recognition Science
This definition feeds the coherence energy E_coh_rs := phiRung (-5) and the gap-45 rung in RSNativeUnits, plus the additive and negation lemmas for integer rungs. It fills the mass formula yardstick · φ^(rung - 8 + gap(Z)) on the φ-ladder and enables the RS entropy and temperature formulas for ultramassive black holes. It connects directly to the eight-tick octave and the Recognition Composition Law.
scope and limits
Does not restrict the rung to integer values.
Does not prove uniqueness of the decomposition.
Does not apply to zero or negative masses.
Does not perform unit conversion to SI.
formal statement (Lean)
217noncomputable def phiRung (M M₀ : ℝ) : ℝ :=
proof body
Definition body.
218 Real.log (M / M₀) / Real.log phi 219 220/-- The φ-rung recovers the mass: M₀ · φ^(phiRung M M₀) = M. -/
used by (22)
From the project-wide theorem graph. These declarations reference this one in their body.