TidalDeform3Cert
plain-language theorem explainer
Certificate packing three structural properties of the RS gravity domain cost used for tidal deformability: vanishing on the diagonal, nonnegativity for positive parameters, and a strictly positive canonical threshold. Gravity session-3 cites it to inhabit the tidal-deformability certificate. Pure structure definition; no proof body.
Claim. A certificate consisting of three facts: (i) the domain cost $C(r,r)=0$ for every nonzero real radius $r$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $T$ satisfies $T>0$.
background
Module RS Gravity (session 3) is a structural theorem package (zero sorry, zero axiom) aimed at neutron-star tidal deformability. Nuclear-structure estimates put $\Lambda_T$ in roughly $500$–$1000$; Recognition Science identifies $\Lambda_T=\varphi^k$ with $\varphi^{13}\approx 521$, so the match is order-of-magnitude consistent.
The domain cost is the local cost functional on mass/eccentricity (or radius) pairs that the gravity layer uses in place of a free potential. Its nonnegativity is the gravity-side shadow of the foundation fact that every recognition event has nonnegative $J$-cost (ObserverForcing cost_nonneg, via $J(x)\ge 0$ for $x>0$). The diagonal identity $C(r,r)=0$ encodes that a matched self-comparison carries zero defect. The canonical threshold is the positive cutoff against which deformability is scored.
Sibling lemmas in the same module discharge each field: diagonal vanishing, nonnegativity, and positivity of the threshold.
proof idea
No proof body: this is a structure (propositional bundle). The three fields are Prop-valued requirements. Downstream, cert assembles an inhabitant by plugging in the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. cert_inhabited is then the one-line Nonempty witness $\langle\texttt{cert}\rangle$.
why it matters
Gives the typed interface that session-3 gravity uses to claim a closed tidal-deformability certificate. Downstream cert and cert_inhabited exist only to show the structure is inhabited, converting three local cost lemmas into a single Nonempty fact for the gravity layer.
In the broader RS picture this sits under the gravity specialization of the $J$-cost calculus (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), with the numerical target $\Lambda_T\sim\varphi^{13}\approx 521$ aligning to the observed NS band. It does not itself derive $\varphi^{13}$; it packages the cost axioms needed before that identification is used.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.