SupernovaType
plain-language theorem explainer
The inductive definition enumerates the five canonical supernova classes Ia, Ib, Ic, IIP and IIL that Recognition Science assigns to configuration dimension D equals 5. Astrophysicists working inside the RS framework cite this enumeration when mapping observed light-curve decline rates onto the phi-ladder. The declaration is a plain inductive type whose automatic derivations supply decidable equality and finite cardinality.
Claim. The finite set of supernova types consists of five elements: Ia (thermonuclear), Ib, Ic, IIP (plateau light curve) and IIL (linear decline), equipped with decidable equality, representation, boolean equality and finite type structure.
background
The module treats supernovae as a five-class system that realizes configDim D = 5 inside Recognition Science. The five classes are Type Ia (thermonuclear), Type Ib, Type Ic, Type II-P and Type II-L, with their light-curve decline timescales placed on the phi-ladder. This supplies the base enumeration from which cardinality statements and certification structures are constructed.
proof idea
The declaration is the inductive definition itself. Lean derives the instances DecidableEq, Repr, BEq and Fintype directly from the five-constructor inductive structure.
why it matters
The definition supplies the five-element set required by the downstream structure SupernovaCert (which asserts Fintype.card equals 5) and by the theorem supernovaType_count (proved by decide). It realizes the five canonical classes (= configDim D = 5) stated in the module documentation and connects to the Recognition Science treatment of astrophysical phenomena on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.