cert
plain-language theorem explainer
Packages the three positivity and identity properties of the stellar-population domain cost into a single certificate record. Astrophysicists citing the D=3 count-law origin of the seven Morgan–Keenan classes use this witness. The body is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There exists a stellar-population certificate: the domain cost vanishes on the diagonal ($C(r,r)=0$ for $r\neq 0$), is nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive.
background
The module treats Morgan–Keenan spectral classes as a structural consequence of configuration dimension $D=3$: the seven main types O, B, A, F, G, K, M equal $2^3-1$, i.e. the nonzero vectors in an $\mathbb{F}_2^3$ temperature/luminosity space (Count Law at $D=3$, forced by T8 in the unified forcing chain).
domainCost is the local cost functional on mass–energy pairs; the certificate demands it be a genuine cost (zero on equal arguments, nonnegative off the axes). canonicalThreshold is the positive cutoff used to separate population bins. Upstream, cost_nonneg from ObserverForcing records that every recognition-event cost is nonnegative via $J$-cost nonnegativity, the same $J(x)=(x+x^{-1})/2-1$ fixed at T5.
proof idea
One-line structure instance. The three fields of StellarPopCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work.
why it matters
Supplies the inhabited certificate that the stellar-population module is structurally sound (status line: 0 sorry, 0 axiom). It anchors the claim that the seven MK classes are forced by $D=3$ rather than fitted, tying astrophysical taxonomy to T8 (three spatial dimensions) and the eight-tick octave count law. No downstream consumers are recorded yet; the companion cert_inhabited is the natural next witness that the type is nonempty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.