stellarEvolutionCert
plain-language theorem explainer
Stellar evolution for sun-like stars is certified to traverse exactly five phases by this definition. Astrophysicists embedding Recognition constraints into stellar models cite it to fix the phase count at five. The construction directly assigns the result of the cardinality theorem for the phase type.
Claim. The stellar evolution certificate is the structure instance satisfying $Fintype.card StellarPhase = 5$, realized by direct assignment of the enumerated cardinality.
background
The module fixes five canonical phases for sun-like stars under Recognition Science: protostar, main sequence, red giant branch, asymptotic giant branch, and white dwarf (or supernova remnant for high-mass cases). This matches the configuration dimension set to five. The structure StellarEvolutionCert encodes solely the requirement that the stellar phase set has cardinality five.
proof idea
One-line definition that populates the StellarEvolutionCert record by direct assignment of the value from the sibling theorem proving the cardinality equals five via exhaustive enumeration.
why it matters
This supplies the phase-count component consumed by the Astronomy module's stellarEvolutionCert to complete its full certificate (including threshold). It implements the five-phase stipulation stated in the module documentation and connects to the Recognition framework by fixing discrete counts from the configuration dimension parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.