cert
plain-language theorem explainer
Packages three domain-cost facts (vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive) into one certificate for the recognition-horizon model. Gravity workers cite it as the bundled witness that the J-cost domain setup is well-formed. The body is a structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
This module treats the black-hole apparent horizon as a level set of the recognition cost: $J(r_H)=J(\varphi)$ at the bounce rung, so the horizon is the $J(\varphi)$-surface of the cost function in curved spacetime. Status is structural (zero sorry, zero axiom).
The certificate structure RecogHorizon3Cert packages three well-formedness conditions on a domain cost $C(m,e)$: diagonal vanishing, nonnegativity for positive mass and energy, and positivity of a canonical threshold. Upstream, nonnegativity of recognition cost is the standard fact that $J$-cost is nonnegative on positive states (ObserverForcing / Cost).
Sibling lemmas supply the three fields: diagonal identity for the domain cost, its nonnegativity, and positivity of the canonical threshold used as the horizon cut.
proof idea
One-line structure instance. Fill cost_at_eq by the sibling diagonal lemma, cost_nonneg by the sibling nonnegativity lemma, and threshold_pos by the sibling positivity lemma for the canonical threshold. No new algebra; pure packaging.
why it matters
Gives a single named witness that the domain-cost model behind the J-cost apparent horizon is coherent: cost vanishes when the two arguments match, never goes negative in the physical quadrant, and the threshold that marks the horizon level is strictly positive. That matches the module claim that the BH horizon is the $J(\varphi)$-level surface of recognition cost (linked to T5 J-uniqueness and the $\varphi$-ladder). No downstream consumers are recorded yet; the certificate is the local handoff point for any later horizon or bounce-rung theorem that needs the three axioms in one place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.