cert
plain-language theorem explainer
Packages three structural facts about the domain J-cost (vanishes on the diagonal, is nonnegative for positive mass/energy, and has a strictly positive canonical threshold) into one gravitational-entanglement certificate. Cite it when wiring ER=EPR to the RS recognition cost. The body is a pure structure instance that plugs three already-proved sibling lemmas into the certificate fields.
Claim. There is a certificate asserting: (i) the domain cost of equal nonzero parameters vanishes, $\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.
background
The module treats gravitational entanglement as a structural consequence of the RS J-cost. Under the ER=EPR reading, an Einstein-Rosen bridge is entanglement, and $J(\phi)$ is the recognition coupling between the two sides; entanglement entropy is written $J(\phi)\cdot(\mathrm{bridge_area}/\ell_{\mathrm{Pl}}^2)$.
The certificate structure bundles three elementary properties of a domain-level cost built from the RS cost functional $J$. Sibling lemmas already show that this domain cost is zero when its two arguments coincide (nonzero), is nonnegative on the positive quadrant, and that a fixed positive threshold (the canonical threshold) sits above zero. Upstream, nonnegativity of recognition-event cost is the standard fact that $J\ge 0$ on positive states.
Local status is a structural theorem package: zero sorry, zero axioms, importing only constants and the cost layer.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas that already prove diagonal vanishing of the domain cost, its nonnegativity for positive mass and energy arguments, and positivity of the canonical threshold. No new algebra is performed; the definition is pure packaging.
why it matters
Gives a single named inhabitant of the gravitational-entanglement certificate so downstream gravity arguments can assume the three J-cost structural facts without re-proving them. It sits inside the Plan-v7 structural theorem that links ER=EPR to the RS recognition coupling $J(\phi)$. The module frames entanglement entropy as $J(\phi)$ times bridge area in Planck units, so this certificate is the minimal cost-side interface that story needs. No parent theorems currently depend on it in the graph; it is the export point of the module's cost hypotheses. Framework landmarks in play are the J-cost (T5 uniqueness of $J$) and the gravity-side reading of recognition coupling across an ER bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.