cert
plain-language theorem explainer
Packages three structural facts about the astrophysics domain cost into a single certificate for the Chandrasekhar module: diagonal vanishing, non-negativity on positive arguments, and a strictly positive canonical threshold. Anyone citing the exact Chandrasekhar mass relation φ^{-1}·2.33 M_⊙ = 1.440 M_⊙ will want this bundle. The definition is a pure structure inhabitant that wires three already-proved sibling lemmas.
Claim. There exists a certificate asserting: (i) the domain cost of any nonzero real $r$ against itself vanishes, $\mathrm{domainCost}(r,r)=0$; (ii) for all positive masses and energies $m,e>0$, $\mathrm{domainCost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
RS Astrophysics Module 2 targets the Chandrasekhar white-dwarf mass limit in Recognition Science units, claiming the exact identity $\phi^{-1}\cdot 2.33,M_\odot = 1.440,M_\odot$ as a structural theorem (zero sorry, zero axiom). The local cost functional is the domain cost on pairs of positive reals (mass and energy scales), built from the global J-cost $J(x)=(x+x^{-1})/2-1$ of the forcing chain.
The certificate structure collects the three elementary properties any such cost must satisfy before threshold comparisons are meaningful: vanishing on the diagonal (perfect match costs nothing), non-negativity for positive arguments, and positivity of the canonical threshold against which excess cost is measured. Upstream, the foundation result that every recognition-event cost is non-negative (via $J\ge 0$ for $x>0$) supplies the moral template for the domain-level non-negativity lemma wired here.
proof idea
One-line structure inhabitant. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity on positive reals), and canonicalThreshold_pos (strict positivity of the threshold). No additional algebra is performed; the definition only assembles those proofs into the record type.
why it matters
Gives the module a single named witness that the cost infrastructure is well-formed before any Chandrasekhar-scale comparison is stated. In the Recognition framework this sits under the astrophysics layer that imports Constants and Cost, and ultimately rests on T5 J-uniqueness and the non-negativity of J. With zero downstream users recorded yet, the certificate is the local gate: later exact-mass or stability statements in this module are expected to take it as a hypothesis or ambient fact rather than re-proving the three elementary properties. It closes no open scaffold; it is the packaging step for an already-proved structural block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.