supernovaCert
plain-language theorem explainer
supernovaCert supplies the concrete witness that exactly five supernova types exist in the Recognition Science classification. Astrophysicists modeling light-curve decline on the phi-ladder would cite this certificate when invoking the five-class taxonomy. The definition is a direct one-line assignment of the cardinality result obtained by exhaustive enumeration.
Claim. Let $S$ be the finite set of supernova types. The structure requires $|S|=5$. The definition instantiates this structure by setting the cardinality field to the theorem value establishing $|S|=5$.
background
The module derives supernova classification from Recognition Science, positing five canonical classes (Type Ia thermonuclear, Ib, Ic, II-P, II-L) that match configDim D=5. Light-curve decline timescales sit on the phi-ladder. The structure SupernovaCert encodes the single assertion that the finite cardinality of the supernova type set equals five.
proof idea
One-line wrapper that populates the five_types field of the SupernovaCert structure with the result of the upstream theorem supernovaType_count.
why it matters
This definition closes the classification certificate inside the SupernovaClassificationFromRS module. It supplies the concrete five-type count required for any RS-based astrophysics application that invokes the phi-ladder for light curves. No downstream uses are recorded and no open questions are flagged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.