cert
plain-language theorem explainer
Packages three elementary facts about the radial domain cost into a single CosmicCensorshipCert record: diagonal vanishing, nonnegativity for positive mass and energy, and a strictly positive bounce threshold. Gravity and RS auditors cite it as the inhabited certificate that weak cosmic censorship holds in the J-cost model. Construction is a pure structure assembly from three sibling lemmas.
Claim. There exists a cosmic-censorship certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive. Together these encode that the J-cost never reaches a naked singularity.
background
The module treats weak cosmic censorship in Recognition Science: classical naked singularities are replaced by a bounce at $r_{\min}=\varphi^{N/2}\ell_{\mathrm{Pl}}>0$. At that radius the J-cost equals $J(\varphi)>0$, so the cost never hits zero and no singularity forms.
Domain cost is the two-argument cost functional on mass and energy (or radial) coordinates used in this gravity layer; its diagonal vanishing and nonnegativity are the local algebraic content of the certificate. The canonical threshold is the positive lower bound that marks the bounce floor.
Upstream, nonnegativity of recognition cost is already forced: any recognition event has cost $\ge 0$ because $J$ itself is nonnegative on positive reals (ObserverForcing). The certificate structure simply packages the gravity-side specializations of that fact.
proof idea
One-line structure construction. The three fields of CosmicCensorshipCert are filled by the sibling lemmas domainCost_at_eq (diagonal identity), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the bounce threshold). No extra tactics or rewriting; the def is pure record assembly.
why it matters
This is the inhabited certificate named by the module's structural theorem (0 sorry, 0 axiom) for weak cosmic censorship from J-cost. It turns the three local cost lemmas into a single named object that downstream gravity arguments can require as a hypothesis or inhabit via cert_inhabited.
In the RS forcing picture the claim sits downstream of T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) and the positivity of $J$ away from the identity: the bounce radius carries $J(\varphi)>0$, so the cost floor never collapses to a singularity. No used_by edges are recorded yet; the certificate is the export surface of the module itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.