supernovaType_count
plain-language theorem explainer
The theorem fixes the cardinality of the supernova classification type at five. Astrophysicists using Recognition Science for transient modeling cite it to set configDim D equal to five when placing light-curve timescales on the phi-ladder. The proof is a one-line decision procedure that exhausts the inductive constructors.
Claim. The finite set of supernova types has cardinality five: $|$SupernovaType$| = 5$, where the five elements are the canonical classes Type Ia, Ib, Ic, II-P, and II-L.
background
SupernovaType is the inductive type whose five constructors are typeIa, typeIb, typeIc, typeIIP, and typeIIL. The module sets this cardinality equal to configDim D = 5 for supernova classification, with light-curve decline timescales located on the phi-ladder. The sole upstream result is the inductive definition of SupernovaType itself.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute Fintype.card directly from the inductive definition of SupernovaType.
why it matters
The result supplies the five_types field required by the downstream supernovaCert definition. It anchors the astrophysics module to the Recognition Science framework by fixing D = 5 for supernovae and linking to the phi-ladder, consistent with the T0-T8 forcing chain and the overall derivation of constants in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.