cert
plain-language theorem explainer
Packages a certificate that the domain cost used for gravitational-wave memory vanishes on equal arguments, stays non-negative for positive mass and energy, and that the canonical threshold is strictly positive. Gravity and RS auditors cite it as the inhabited witness for the structural GW-memory-from-J-cost claim. The body is a three-field structure instance wiring already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical memory threshold is strictly positive.
background
The module treats gravitational-wave memory as a J-cost effect: the permanent strain offset is $\delta h = J(\varphi),h_{\mathrm{peak}}$ for the canonical memory fraction. Recognition Science identifies memory with $J(\varphi)$ of peak strain; empirically memory is roughly 5–15% of peak, and $J(\varphi)\approx 11.8%$ sits inside that band.
Domain cost is the local cost functional on positive reals used to score recognition mismatch in this gravity setting. The certificate structure demands three elementary properties of that cost and of the canonical threshold: diagonal vanishing (equal arguments cost nothing), nonnegativity for positive arguments, and a strictly positive threshold. Upstream, the foundation result that every recognition-event cost is nonnegative (via nonnegativity of $J$) supplies the same sign discipline used here.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas that already prove diagonal vanishing of domain cost, nonnegativity of domain cost on positive arguments, and positivity of the canonical threshold. No extra algebra is performed at this site.
why it matters
This definition is the inhabited witness that the structural GW-memory-from-J-cost package is fully discharged (module status: 0 sorry, 0 axiom). It sits under the Plan v7 gravity line that equates memory fraction with $J(\varphi)$, tying the permanent strain offset to the unique J-cost forced in the T5 step of the forcing chain and to the golden ratio fixed point from T6. With no further used-by edges in the graph, its role is to close the local certificate rather than feed a larger named theorem; together with the sibling inhabitedness lemma it makes the certificate available as a first-class object for any later gravity or observational comparison that needs the three cost axioms in one place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.