RSAstro001Cert
plain-language theorem explainer
Certificate bundle for Astrophysics RS Module 1: the domain cost vanishes on the diagonal, stays non-negative for positive mass/energy arguments, and the canonical threshold is strictly positive. Downstream code cites the inhabited instance to lock the solar-surface-temperature structural claim (φ¹⁸ K = 5778 K). The declaration is a pure structure packing three Prop fields; no proof lives here.
Claim. A certificate for Astrophysics Module 1 consists of three facts: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e>0$, one has $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
Module 1 of the RS astrophysics layer targets the solar surface temperature identity $\varphi^{18},\mathrm{K}=5778,\mathrm{K}$ (PDG exact match), packaged as a structural theorem with zero sorry and zero axiom. The local cost is a domain-level specialization of the Recognition J-cost: it measures mismatch between a model scale and an evidence scale on positive reals.
Upstream, the foundation result cost_nonneg states that every recognition event has non-negative cost, via non-negativity of $J$. The certificate fields mirror that discipline at the astrophysics interface: diagonal vanishing (perfect match costs nothing), positivity off the match, and a strictly positive decision threshold used to gate the temperature claim.
Sibling defs supply the concrete domainCost and canonicalThreshold together with the three lemmas that will inhabit the fields.
proof idea
No proof body: this is a structure declaration. It only names the three Prop fields that any valid certificate must supply. Inhabitation is deferred to the downstream cert definition, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively.
why it matters
The structure is the typed gate for Module 1. Downstream cert builds a concrete inhabitant, and cert_inhabited records Nonempty RSAstro001Cert, which is the formal hook that the solar-temperature structural theorem is certified rather than assumed. In the broader RS chain this sits under the cost calculus forced by T5 (J-uniqueness) and the φ-ladder used for rung-to-kelvin conversion; the module claims an exact PDG match at rung 18. Without this certificate type, later astrophysics modules cannot uniformly demand cost-well-posedness and a positive threshold before quoting observational equalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.