cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single GW Phase-3 certificate: diagonal cost vanishes, cost is nonnegative off the identity, and the canonical threshold is positive. Gravity and PN-phase workers cite it as the inhabited witness that the J-cost side of the structural GW-phase story is well-formed. The body is a three-field structure instance wiring 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 threshold is strictly positive.
background
The module treats gravitational-wave phase evolution as a structural consequence of the Recognition Science J-cost. In RS units the leading PN phase coefficient is tied to $\phi^{D-1}=\phi^2\approx 2.618$ (with $D=3$), giving the schematic form $\Psi=-\phi^{D-1}(f/f_{\mathrm{merger}})^{-5/3}$. Status is structural: zero sorry, zero axioms.
Domain cost is the local cost functional on mass/energy-like pairs used to gate the phase story. The certificate structure GWPhase3Cert demands three properties of that cost and of a fixed positive threshold: vanishing on the diagonal (equal arguments), nonnegativity for positive arguments, and positivity of the threshold. Upstream, the global recognition cost is already known to be nonnegative (cost_nonneg: cost of any recognition event is $\ge 0$, via $J$-cost nonnegativity).
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive inputs), and canonicalThreshold_pos (strict positivity of the threshold). No further rewriting or case analysis.
why it matters
Gives an inhabited, zero-sorry witness that the J-cost side of the GW Phase-3 structural package is consistent. The module frames this as the RS reading of the leading-order PN phase coefficient via $\phi^{D-1}=\phi^2$, linking the eight-tick / $D=3$ forcing chain (T7–T8) to chirp-mass scaling. No downstream dependents are recorded yet; the sibling cert_inhabited is the natural next consumer. It does not itself derive the phase formula $\Psi$, only certifies the cost/threshold hypotheses the structural story needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.