rs_entropy
plain-language theorem explainer
RS entropy for a black hole in native units is the product of the recognition Boltzmann constant and the count of Planck-area cells on the horizon. Researchers deriving black hole thermodynamics or entropy scaling in Recognition Science cite this when establishing mass-squared dependence. The definition is a direct multiplication of k_R by the cell count derived from horizon area.
Claim. For a black hole with positive mass $M$ in RS-native units, the entropy is $S = k_R · A/(4ℓ_0^2)$, where $k_R = ln φ$ is the cost per recognition event, $A = 4π(2GM)^2$ is the horizon area, and $ℓ_0$ is the fundamental length.
background
The UltramassiveBH module treats black holes as RSBH structures carrying only a positive mass in units where $c = ℓ_0 = τ_0 = 1$. The recognition Boltzmann constant $k_R$ equals $ln φ$, the fundamental cost per ledger bit that replaces $k_B$ in RS thermodynamics. Horizon cell count is the horizon area divided by $4ℓ_0^2$, so each cell registers one recognition event.
proof idea
One-line definition that multiplies $k_R$ by the horizon cell count. The cell count itself expands to horizon area over $4ℓ_0^2$, inheriting the area formula from the Schwarzschild radius without further lemmas.
why it matters
Supplies the entropy field inside the UltramassiveBHCert bundle and is invoked by the theorems that entropy quadruples on mass doubling and that entropy is positive. It directly encodes the RS entropy formula $S_{BH} = (ln φ) · A/(4ℓ_0^2)$ stated in the module documentation, tying black-hole thermodynamics to the recognition cost $k_R = ln φ$ and the underlying J-cost functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.