rs_entropy_eq
plain-language theorem explainer
The theorem states that RS entropy of a black hole equals k_R times horizon area divided by 4 ell0 squared. Researchers deriving black hole thermodynamics from the J-cost ledger in Recognition Science would cite this for the entropy-area relation. The proof is a one-line reflexivity that holds because rs_entropy is defined to match the right-hand side exactly.
Claim. For a black hole $bh$ in RS-native units with positive mass, the recognition entropy satisfies $S_{RS}(bh) = k_R · (A_h(bh) / (4 ℓ_0²))$, where $k_R = ln φ$ is the recognition Boltzmann constant and $ℓ_0$ is the fundamental length unit.
background
RSBH is the structure for a black hole in native units where c = ℓ₀ = τ₀ = 1 and mass > 0. The module sets the RS entropy formula as S_BH = (ln φ) · A / (4 ℓ₀²) with k_R defined as ln φ, the cost per ledger bit. ell0 is the fundamental length (voxel) set to 1. Upstream, entropy is defined as total defect of a configuration, and k_R is shown positive since φ > 1.
proof idea
The proof is a term-mode reflexivity. It holds because the left-hand side rs_entropy bh is defined to be identical to the right-hand side expression involving k_R and horizonArea bh.
why it matters
This theorem realizes the RS entropy formula listed as key result 2 in the module documentation for ultramassive black holes. It specializes the general entropy definition (proportional to total defect) to the horizon cells counted by horizonArea. In the Recognition Science framework it supplies the entropy-area law that supports the no-singularity claim and the cold Hawking temperature for large masses. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.