GWMemory3Cert
plain-language theorem explainer
Certificate bundling three structural properties for gravitational-wave memory from J-cost: diagonal domain cost vanishes, domain cost is nonnegative on positive arguments, and the canonical threshold is positive. Downstream code builds a concrete inhabitant and proves the type is nonempty. Pure structure definition with no proof body.
Claim. A certificate consists of three facts: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and 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 that fraction with $J(\varphi)\approx 11.8%$, inside the empirical $5$–$15%$ band of peak strain.
domainCost is the local cost functional on mass/energy (or ratio) parameters used in this gravity module; the certificate demands it vanish on the diagonal and stay nonnegative off it. canonicalThreshold is the positive scale against which the memory fraction is compared. Upstream, the foundation lemma cost_nonneg already asserts that every recognition-event cost is nonnegative via $J$-cost nonnegativity, which this certificate mirrors at the domain level.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. The sibling definition cert fills them by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then packages ⟨cert⟩ as a Nonempty witness.
why it matters
Gives the typed interface for the module’s structural theorem (zero sorry, zero axiom) that GW memory is forced by J-cost. Downstream, cert inhabits the structure and cert_inhabited records nonemptiness, so later gravity results can assume the three properties by projecting fields rather than re-proving them. Ties the memory fraction to the T5 J-uniqueness cost $J(x)=(x+x^{-1})/2-1$ evaluated at the golden ratio $\varphi$ from T6, keeping the claim inside the RS forcing chain rather than an ad-hoc strain fit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.