entropy_quadruples_on_double
plain-language theorem explainer
RS entropy for black holes scales quadratically with mass in Recognition Science. A physicist deriving horizon information content for ultramassive objects such as TON 618 would cite this scaling when comparing entropy across different masses. The proof is a direct algebraic reduction obtained by unfolding the entropy, cell-count, area, and radius definitions then substituting the mass-doubling hypothesis.
Claim. Let $bh_1$ and $bh_2$ be RS black holes with positive masses. If the mass of $bh_2$ equals twice the mass of $bh_1$, then the RS entropy of $bh_2$ equals four times the RS entropy of $bh_1$.
background
An RSBH is a structure carrying a positive real mass in RS-native units (length, time, and $c$ all set to 1). The RS entropy is defined as $k_R$ times the number of horizon cells, where $k_R = ln φ$ is the recognition Boltzmann constant giving the information cost per recognition event. Horizon cells equal the horizon area divided by $4ℓ_0^2$, and the area is $4π$ times the square of the Schwarzschild radius, which is proportional to mass. The module documentation states the general formula $S_{BH} = (ln φ) · A/(4ℓ_0^2)$ and lists this scaling as one of the key results for ultramassive black holes.
proof idea
The proof is a term-mode reduction. It unfolds rs_entropy, horizonCells, horizonArea, and schwarzschildRadius to expose the explicit quadratic dependence on mass. The hypothesis that the second mass is twice the first is substituted, after which the ring tactic confirms the resulting polynomial identity.
why it matters
The declaration confirms the quadratic mass scaling that follows directly from the RS area law for black-hole entropy. It supports the module's stated results on RS entropy and Hawking temperature for ultramassive objects and aligns with the Recognition Science entropy formula $S_{BH} = (ln φ) · A/(4ℓ_0^2)$. The result is consistent with the framework's derivation of constants in RS-native units but does not invoke the forcing-chain steps T0-T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.