phiRung
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.