phi_ladder_recovery
plain-language theorem explainer
The φ-rung recovery theorem shows that any positive mass M is recovered exactly by scaling a reference mass M₀ by φ raised to the exponent phiRung(M, M₀). Researchers modeling ultramassive black holes on the Recognition Science φ-ladder cite it to guarantee mass consistency before deriving entropy or temperature formulas. The proof is a direct algebraic cancellation: unfold the rung as the base-φ log of the mass ratio, rewrite the power via exp-log, and simplify.
Claim. For all real numbers $M, M_0 > 0$, $M_0 · φ^{rung(M,M_0)} = M$, where $rung(M,M_0)$ denotes the real exponent on the φ-ladder satisfying the scaling relation.
background
In the Recognition Science treatment of ultramassive black holes, masses are placed on the φ-ladder so that a base mass M₀ scales to target M via integer or real powers of φ. The function phiRung computes this exponent as log_φ(M/M₀). The module derives no-singularity results, RS entropy S_BH = (ln φ)·A/(4ℓ₀²), and Hawking temperature from J-cost finiteness on (0,∞). Upstream, one_lt_phi supplies 1 < φ so that log φ is positive and nonzero; the constants module defines phiRung and native units with c=1, ħ=φ^{-5}.
proof idea
Unfold phiRung to obtain the explicit form log(M/M₀)/log φ. Rewrite φ raised to this power as exp(log φ · (log(M/M₀)/log φ)) using the real-power definition. The displayed identity and field_simp cancel the log φ factors, after which exp_log reduces the expression to M/M₀. The auxiliary fact one_lt_phi ensures division by log φ is valid.
why it matters
The theorem anchors mass recovery on the φ-ladder inside the ultramassive-BH module, directly supporting the claim that black-hole interiors are maximal J-cost states rather than curvature singularities. It enables the RS entropy and temperature formulas by guaranteeing consistent scaling. In the framework it instantiates T5–T6 (J-uniqueness and φ fixed point) for gravitational objects and aligns with the mass formula yardstick·φ^(rung−8+gap(Z)). No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.