cert
plain-language theorem explainer
Packages three structural facts about the black-hole domain cost into one certificate: the cost vanishes on the mass-energy diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Gravity and RS auditors cite it as the inhabited witness that the J-cost side of the BH entropy log-correction is well-posed. The body is a pure structure assembly of three sibling lemmas.
Claim. There exists a certificate recording that the domain cost $C(m,e)$ satisfies $C(r,r)=0$ for all $r\neq 0$, $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and the canonical threshold $t_*$ obeys $t_*>0$.
background
This module treats the black-hole entropy logarithmic correction as a structural consequence of the Recognition Science J-cost. The module status line records a zero-sorry, zero-axiom structural theorem whose RS-native coefficient is $c_{\mathrm{RS}}=-\log\varphi/2\approx -0.2406$, matching Sen's 2013 Kerr-Newman 4D value exactly and Falls-Litim 2014 asymptotic-safety numerics to three digits.
The domain cost is the two-argument cost used on the mass-energy plane; the certificate structure BHEntropyLog2Cert packages the three elementary properties needed before any entropy formula is stated: vanishing on the diagonal $m=e$, nonnegativity for positive mass and energy, and positivity of a canonical threshold. Upstream, the general recognition cost is already known to be nonnegative (cost_nonneg: "The cost of any recognition event is non-negative"), via nonnegativity of $J$.
proof idea
One-line structure inhabitant. The three fields of BHEntropyLog2Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity on the positive quadrant), and canonicalThreshold_pos (threshold positivity). No extra algebra is performed at this site.
why it matters
Gives the inhabited certificate that the J-cost side of the BH entropy log-correction is structurally sound before numerical comparison. The module claims exact agreement with Sen 2013 ($c=-\log\varphi/2$) and near-agreement with Falls-Litim 2014 asymptotic safety ($\sim -0.241$), with an RS_PASS flag. No downstream consumers are wired yet in the graph; the sibling cert_inhabited is the natural next witness. Sits in the gravity layer that imports Constants and Cost, so it inherits the forced $J$ from the T5 uniqueness step and the golden-ratio fixed point from T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.