cert
plain-language theorem explainer
Packages three field lemmas into an inhabited Penrose-from-J-cost certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Gravity and RS black-hole geometry work cites this as the structural witness that the J-cost setup is well-posed. Construction is a pure structure literal; no new mathematics.
Claim. There is a certificate asserting: (i) the domain cost satisfies $C(r,r)=0$ for every $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
The module derives a Recognition-Science form of the Penrose inequality from the J-cost. Classically one has $M\ge\sqrt{A/(16\pi)}$; in RS the black-hole bounce geometry inserts a $\phi^{1/2}$ factor, so $M\ge\phi^{1/2}\sqrt{A/(16\pi)}$. Status is structural: zero sorry, zero axiom.
Domain cost is the local cost functional on mass/energy-type coordinates used to encode the inequality. The J-cost $J(x)=(x+x^{-1})/2-1$ (forced at T5) is nonnegative and vanishes only at the identity $x=1$; upstream cost_nonneg records that every recognition event has nonnegative cost via Jcost_nonneg.
PenroseIneqCert is the structure bundling the three well-posedness obligations: diagonal vanishing of domain cost, nonnegativity off the diagonal for positive arguments, and positivity of the canonical threshold that sets the geometric scale.
proof idea
One-line structure construction. The three fields of PenroseIneqCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No tactics and no new proof obligations; the definition is the inhabited certificate itself.
why it matters
Gives the concrete witness that the J-cost setup for the Penrose inequality is well-posed inside RS gravity. The module frames this as a structural theorem (Plan v7 final session) linking the classical area-mass bound to the forced cost $J$ and the golden-ratio correction from bounce geometry. Downstream consumers (none listed yet on this edge set) would discharge hypotheses of the form "assume a PenroseIneqCert" by pointing at this value, or use cert_inhabited. Ties to T5 J-uniqueness and the RS constants ($c=1$, $\hbar=\phi^{-5}$, $G=\phi^5/\pi$) only indirectly: the cost nonnegativity lineage runs through ObserverForcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.