cert
plain-language theorem explainer
Packages three elementary facts about the gravity-domain cost into a single tidal-deformability certificate: the cost vanishes on equal arguments, stays non-negative for positive mass and energy, and the canonical threshold is positive. Gravity and neutron-star modelers cite it as the inhabited witness that the RS cost setup is well-posed for Lambda_T comparisons. The body is a pure structure assembly from three prior lemmas.
Claim. There exists a tidal-deformability certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module develops Recognition Science gravity as a structural theorem layer (zero sorry, zero axiom). The physical target is neutron-star tidal deformability: observations give $\Lambda_T\sim 500$–$1000$, while RS predicts a pure $\phi$-power $\Lambda_T=\phi^k$ with $\phi^{13}\approx 521$, hence consistency near $500$.
The certificate structure TidalDeform3Cert packages three well-posedness conditions on a domain cost functional used for that comparison: diagonal vanishing, non-negativity on the positive quadrant, and a positive decision threshold. Non-negativity is the gravity-side shadow of the global fact that every recognition event has non-negative J-cost (ObserverForcing: "The cost of any recognition event is non-negative").
Canonical threshold positivity supplies the numerical gate against which the $\phi^{13}$ ladder value is later compared.
proof idea
One-line structure inhabitant. The three fields are filled by the already-proved sibling facts domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No new algebra is performed; the definition merely witnesses that those three lemmas jointly satisfy the certificate interface.
why it matters
Gives an inhabited, zero-sorry certificate that the RS gravity cost setup is mathematically well-posed before any numerical $\Lambda_T$ claim is stated. The module status line treats the whole session as a structural theorem supporting the match $\Lambda_T\sim\phi^{13}\approx 521$ against the observational band $500$–$1000$. Downstream consumers (none yet recorded in the graph) can take cert as a single hypothesis package rather than three separate lemmas. It sits inside the broader RS constants story ($\phi$ forced at T6, eight-tick octave at T7) by supplying the cost hygiene needed for a gravity-side $\phi$-ladder comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.