GravEntropy2Cert
plain-language theorem explainer
Certificate packing three structural hypotheses for gravitational entropy from J-cost: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy, and the canonical threshold is positive. Gravity and entropy-production arguments cite it to discharge well-posedness before the BH log correction. Pure structure definition; inhabitants are assembled elsewhere from sibling lemmas.
Claim. A gravitational-entropy certificate is a record of three assertions: (i) the domain cost $C$ satisfies $C(r,r)=0$ for every nonzero real $r$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $\tau$ is strictly positive.
background
The module derives gravitational entropy production from the Recognition Science J-cost, targeting the black-hole log correction $S_{\mathrm{BH}}=A/(4\ell_{\mathrm{Pl}}^2)-(\log\phi)/2\cdot\log(A/\ell_{\mathrm{Pl}}^2)$, with $c_{\log}=-\log\phi/2$ read off recognition-bundle curvature. Status is structural (zero sorry, zero axiom).
Domain cost is the local cost functional on mass/energy-type reals used in this gravity layer; the certificate demands it vanish when the two arguments coincide (identity recognition) and stay nonnegative off that diagonal for positive inputs. The canonical threshold is the positive scale against which entropy production is compared.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity on positive states. That global fact is the template for the domain-cost nonnegativity field here.
proof idea
No proof body: this is a structure whose fields are propositions. An inhabitant is built by the sibling definition cert, which plugs in domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Nonemptiness is then the one-line theorem cert_inhabited wrapping that witness.
why it matters
Gives a single named interface for the three positivity/vanishing facts the gravitational-entropy-from-J-cost development needs before quoting the BH area law with RS log correction. Downstream, cert inhabits the structure and cert_inhabited exports Nonempty GravEntropy2Cert, so later gravity lemmas can assume the certificate rather than re-prove diagonal vanishing and threshold positivity. Ties the gravity layer to the J-cost minimum at identity (primer T5) and to the $\phi$-dependent curvature coefficient in the module doc. Closes the structural side of Plan v7's 122nd-pass entropy production claim without introducing axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.