rs_entropy_pos
plain-language theorem explainer
RS entropy positivity asserts that every black hole formalized as an RSBH with positive mass has strictly positive recognition entropy. Black-hole thermodynamics researchers in Recognition Science cite it to confirm the entropy formula remains positive for ultramassive objects such as TON 618. The proof is a short term-mode chain that unfolds the entropy definition and applies positivity of k_R, G, ell0 and the squared radius term.
Claim. For every black hole $bh$ with mass $m > 0$ in RS-native units, the RS entropy satisfies $S_{BH}(bh) > 0$, where $S_{BH} = k_R A / (4 ell_0^2)$, $A = 4 pi r_s^2$, and $r_s = 2 G m$.
background
The UltramassiveBH module treats black holes via the RSBH structure, which consists of a positive real mass in units where $c = ell_0 = tau_0 = 1$. RS entropy is defined from the formula $S_{BH} = (ln phi) A / (4 ell_0^2)$, with $k_R = ln phi$ the recognition Boltzmann constant. Upstream lemmas establish the required positivity: k_R_pos (theorem C-006.1) shows $k_R > 0$ because phi > 1, while ell0_pos and G_pos confirm the length and gravitational constants are positive.
proof idea
The term proof unfolds rs_entropy, horizonCells, horizonArea and schwarzschildRadius, then applies mul_pos to k_R_pos and a div_pos whose numerator is 4 pi times the square of (2 G m). Positivity of the numerator follows from mul_pos on (by norm_num : 0 < 4), Real.pi_pos, and sq_pos_of_pos applied to mul_pos of (by norm_num : 0 < 2), G_pos and bh.mass_pos. The denominator is handled by mul_pos on (by norm_num : 0 < 4) and sq_pos_of_pos of ell0_pos.
why it matters
This result supplies the entropy_positive field inside the ultramassiveBHCert certificate, which also records no_singularity, temp_positive and hamiltonian_approximation_bound. It thereby confirms that the RS entropy formula yields positive values for all positive-mass black holes, consistent with the module's no-singularity claim that the interior is a maximal J-cost state. The positivity aligns with the Recognition Science entropy scaling S_BH proportional to area and with the positivity of k_R derived from phi > 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.