SupernovaCert
plain-language theorem explainer
The declaration defines a structure certifying that the Recognition Science supernova classification contains exactly five types. Astrophysicists invoking the RS framework for canonical classes Ia through IIL would cite this when referencing the fixed enumeration. The definition is a direct packaging of the cardinality fact from the inductive type SupernovaType.
Claim. Let $S$ be the inductive type with five constructors corresponding to the canonical supernova classes (Ia, Ib, Ic, II-P, II-L). The structure SupernovaCert consists of the single field asserting that the cardinality of the finite type $S$ equals 5.
background
In the module on Supernova Classification from RS, the framework posits five canonical supernova classes corresponding to a configuration dimension of 5. These are Type Ia (thermonuclear), Type Ib, Type Ic, Type II-P, and Type II-L, with light-curve decline timescales placed on the phi-ladder. The upstream inductive definition SupernovaType enumerates precisely these five variants and derives the Fintype instance used for cardinality.
proof idea
This declaration is a structure definition with an empty proof body. It directly packages the assertion that the Fintype cardinality of SupernovaType equals 5, relying on the derived Fintype instance from the inductive enumeration of the five constructors.
why it matters
This structure supplies the certification required by the downstream definition supernovaCert, which constructs an explicit instance via the Fintype count. It establishes the five-type classification within the RS astrophysics module, aligning with the framework's configuration dimension and phi-ladder placement for timescales. It touches the open question of deriving explicit light-curve behaviors from the J-cost and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.