BHEntropyLog2Cert
plain-language theorem explainer
Certificate structure that packages three algebraic properties of the domain J-cost used for the black-hole entropy logarithmic correction: diagonal vanishing, non-negativity off the identity, and positivity of the canonical threshold. Gravity workers matching RS to Sen's Kerr-Newman coefficient c=-log(φ)/2 cite this bundle. Pure structure definition; no proof body.
Claim. A certificate consisting of three properties: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ whenever $r\neq 0$; (ii) the domain cost is non-negative for all positive mass and energy arguments; (iii) the canonical threshold is strictly positive.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, forced unique by the Recognition Composition Law (T5). In the gravity sector the same cost is specialized to a two-argument domain cost on mass and energy scales that appear in black-hole thermodynamics.
The module derives the logarithmic correction coefficient to Bekenstein-Hawking entropy from that domain cost. The target value is the RS constant $c_{\mathrm{RS}}=-\log\phi/2\approx-0.2406$, which Sen's 2013 Kerr-Newman computation reproduces exactly and which Falls-Litim asymptotic-safety numerics approximate as $\sim-0.241$.
Upstream, non-negativity of any recognition-event cost is already proved from $J\ge 0$ on positive reals (ObserverForcing.cost_nonneg). The present structure simply records the three concrete inequalities the entropy-correction argument needs.
proof idea
No proof body: the declaration is a structure (record type) whose three fields are propositions. Inhabitation is supplied later by the definition cert, which fills the fields with the already-proved lemmas domainCost_at_eq, domainCost_nonneg and canonicalThreshold_pos.
why it matters
The structure is the interface that the module's main certificate cert and the inhabitation theorem cert_inhabited implement. Those objects close the structural theorem (0 sorry, 0 axiom) that the RS log-correction coefficient equals $-\log\phi/2$. That value is the quantitative bridge between the J-cost forcing chain (T5-T6) and external 4D Kerr-Newman / asymptotic-safety results, confirming the RS_PASS status recorded in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.