SGWB3Cert
plain-language theorem explainer
Certificate bundle for the third stochastic gravitational-wave background module: domain cost vanishes on the diagonal, is nonnegative for positive mass and energy, and the canonical threshold is positive. Cosmologists working the RS phi-ladder SGWB would cite this as the interface type. It is a pure structure definition with three Prop fields; no proof body.
Claim. A certificate for the third SGWB layer is a triple of facts: (i) for every nonzero real $r$, the domain cost at $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the stochastic gravitational-wave background on the Recognition Science phi-ladder (Plan v7, 117th pass). Status is structural: zero sorry, zero axiom. The RS sketch is $\Omega_{\mathrm{GW}} = J(\varphi)^2 \Omega_{\mathrm{matter}} \approx 0.014 \times 0.315 = 0.0044$, while nHz PTA bands (PPTA/NANOGrav) sit near $10^{-9}$, so the claim is structural rather than a precision fit.
Domain cost is the local cost functional on mass-energy pairs used in this cosmology layer; the diagonal identity says matched arguments carry zero excess cost. Nonnegativity mirrors the foundation fact that recognition cost never goes negative (ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity). The canonical threshold is the positive cutoff against which the background is compared.
The structure packages exactly those three obligations so downstream code can inhabit a single certificate rather than thread three separate lemmas.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued obligations (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Inhabitation is deferred to the sibling cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the typed interface for the structural SGWB certificate in Cosmology.GravitationalWaveBackground3. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty SGWB3Cert, closing the module's structural claim.
In the RS framework this sits under the phi-ladder cosmology layer: J-cost uniqueness (T5), phi as self-similar fixed point (T6), and the eight-tick octave (T7) already fix the cost geometry; the certificate only asserts that the domain cost and threshold used for $\Omega_{\mathrm{GW}}$ obey the same nonnegativity and identity minima. It does not itself derive the $10^{-9}$ nHz amplitude; it certifies the cost-side hypotheses the structural theorem needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.