cert
plain-language theorem explainer
Packages three structural facts about the SGWB domain cost and its threshold into a single certificate record. Cosmologists citing the phi-ladder stochastic GW background use this as the inhabited witness that the cost is a genuine nonnegative defect vanishing on the diagonal. The body is a pure structure assembly: three sibling lemmas are plugged into the three fields.
Claim. There exists a certificate bundling: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and energy arguments; (iii) the canonical threshold is strictly positive.
background
The module treats the stochastic gravitational-wave background (SGWB) as a structural consequence of the phi-ladder. In RS units the predicted amplitude is $\Omega_{\mathrm{GW}}=J(\varphi)^2\Omega_{\mathrm{matter}}\approx 0.0044$, while nHz PTA bands (PPTA/NANOGrav) sit near $10^{-9}$; the gap is left as a structural remark, not a fitted spectrum.
The local cost is a two-argument domain cost built from the Recognition J-cost $J(x)=(x+x^{-1})/2-1$. Upstream, cost_nonneg records that every recognition event has nonnegative cost via $J\ge 0$ for positive states. The certificate structure simply freezes three properties needed downstream: diagonal vanishing, nonnegativity on the positive orthant, and a strictly positive canonical threshold.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No additional rewriting or case analysis occurs.
why it matters
Gives an inhabited witness that the SGWB3 cost interface is well-formed: a nonnegative defect that is zero on matched arguments, with a positive detection threshold. That is the structural backbone of the module's claim that the phi-ladder GW background is a cost-theoretic object rather than a free spectral fit. It sits under the Plan v7 structural theorem (0 sorry, 0 axiom) for $\Omega_{\mathrm{GW}}$ from $J(\varphi)$ and matter density. No downstream consumers are recorded yet; the immediate sibling cert_inhabited is the natural use site. Framework landmarks touched: J-uniqueness (T5) via the cost, and the phi-ladder mass/energy bookkeeping that feeds cosmology amplitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.