RSAstro012Cert
plain-language theorem explainer
Certificate bundle for Astrophysics Module 12 (carbon-oxygen stellar structure). It packages three Prop fields: domain cost vanishes on equal nonzero arguments, is nonnegative for positive mass/energy, and the canonical threshold is positive. Downstream code inhabits it via the module's concrete lemmas. Pure structure definition; no proof body.
Claim. A Module-12 certificate is a record of three facts: (1) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (2) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (3) the canonical threshold is strictly positive.
background
Module 12 is the carbon-oxygen stellar structural claim in the RS astrophysics stack: the C/O abundance ratio is identified with $\phi^{-1.5}\approx 0.504$, compared to the empirical $\sim 0.55$ (about 10% off), and is marked STRUCTURAL with zero sorry and zero axiom.
The certificate talks about a local domain cost (a real-valued cost on mass/energy pairs in this module) and a canonical threshold scalar used as a positivity gate. Upstream, the foundation lemma cost_nonneg states that every recognition event has nonnegative cost, proved from nonnegativity of the J-cost on positive states. That global nonnegativity pattern is mirrored here by the domain-level nonnegativity field.
Sibling lemmas in the same file discharge the three fields: diagonal vanishing, domain nonnegativity, and threshold positivity.
proof idea
No proof: this is a structure declaration whose fields are propositions. Inhabitation is deferred to the downstream definition that fills the three fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The structure itself only names the interface.
why it matters
Gives a typed certificate interface for the C/O stellar module so downstream code can demand the three structural cost/threshold facts in one package. Immediate consumers are the concrete inhabitant cert and the theorem cert_inhabited proving Nonempty of the certificate type.
In the broader RS picture this sits in the astrophysics layer that attaches stellar abundance structure to the $\phi$-ladder (here $\phi^{-1.5}$ for C/O). It does not itself force $\phi$ or the eight-tick octave; those live in the T5–T7 forcing chain. Its role is bookkeeping: a zero-sorry structural certificate that later modules can require when wiring abundance claims to cost positivity and a positive threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.