Pith. sign in
module module high

IndisputableMonolith.Gravity.BlackHoleEntropySI

show as:
view Lean formalization →

SI-unit Bekenstein-Hawking entropy as a function of horizon area, and the matching RS ledger form after the dimensional bridge. Gravity and quantum-gravity workers cite it when comparing RS log-area corrections to LQG and string predictions in laboratory units. The module wires the ledger entropy through the SI bridge and Hawking-temperature SI layer, then records positivity and mass-parameterized equalities.

claimDefine the SI Bekenstein-Hawking entropy $S_{\mathrm{BH}}^{\mathrm{SI}}(A_{\mathrm{SI}}) = k_B^{\mathrm{SI}} \, A_{\mathrm{SI}} \, c_{\mathrm{SI}}^3 / (4 \, G_{\mathrm{SI}} \, \hbar_{\mathrm{SI}})$, the mass-parameterized form $S_{\mathrm{BH}}^{\mathrm{SI}}(M)$, and the RS-bridged entropy $S_{\mathrm{RS}}^{\mathrm{SI}}$. Record positivity, the bridge equality to the leading ledger term, and elementary bounds used for the $\varphi$-rational log correction (e.g. $\log\varphi < 1/2$).

background

Recognition Science recovers black-hole entropy from a discrete ledger: admissible horizon states modulo $\sigma$-equivalence yield $S_{\mathrm{BH}} = A/(4\ell_P^2)$ plus a leading log correction whose coefficient is $\varphi$-rational. That ledger form lives in RS-native units. The SI bridge closure supplies the unique calibration map that converts RS-native quantities into SI once the dimensional anchor is fixed.

This module sits on that bridge and on the SI Hawking-temperature track. It packages the classical area law in SI constants ($k_B$, $c$, $G$, $\hbar$) and the bridged RS entropy so that numerical and theorem-grade comparisons can be stated without unit conversion footnotes. Sibling lemmas also give a mass-parameterized SI entropy and elementary inequalities (such as $\log\varphi < 1/2$) needed when the RS log coefficient is compared to rival predictions.

proof idea

Definition-first module: SI entropy is introduced by the standard area formula in SI constants; the mass form is the same quantity reparameterized by horizon mass; the RS-SI form is the ledger leading term pushed through the SI bridge. Positivity and equality lemmas are short algebraic or bridge applications (bridge equality to the leading ledger term; mass form equals area form). Auxiliary facts such as $\log\varphi < 1/2$ and a lower bound on the RS log coefficient are elementary real inequalities supporting later discriminator comparisons, not deep gravity arguments.

why it matters in Recognition Science

Without an SI packaging of both the classical area law and the RS ledger entropy, the gravity discriminators cannot be stated in the units experimental and rival-theory literature use. Downstream, DiscriminatorCert and DiscriminatorMatrix import this module to run theorem-grade comparisons of the RS $\varphi$-rational log-area coefficient against LQG ($-1/2$) and string theory ($-3/2$). MasterTheorem consumes the same SI layer as part of the conditional gravity master statement (Track 7.A).

The module therefore closes the SI face of Track F6 (entropy from the ledger) and feeds Track 6 discriminators and the master theorem. Framework landmarks in play are the ledger-derived horizon count, the SI bridge closure, and the $\varphi$-structured correction that RS claims is observationally distinguishable from LQG and strings.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (20)