stellarPhaseCount
plain-language theorem explainer
The theorem establishes that the inductive type of canonical stellar phases in the J-cost model has cardinality exactly five. Astrophysicists using Recognition Science to model evolution would cite this to confirm the phase count matches the predicted configDim D=5. The proof is a one-line decide tactic that computes the Fintype.card directly from the five constructors.
Claim. The set of stellar phases has cardinality five: $|$ {main sequence, subgiant, red giant, horizontal branch, remnant} $| = 5$.
background
The Stellar Evolution from J-Cost module treats stellar evolution as a sequence of phase transitions driven by crossings of the canonical J(phi) band. The StellarPhase inductive type lists the five stages (mainSequence, subgiant, redGiant, horizontalBranch, remnant) and derives Fintype, DecidableEq, and related instances to support cardinality and enumeration. Module documentation states that these five phases equal configDim D=5, providing the local theoretical setting. An upstream StellarPhase definition in Astrophysics uses a different five-phase enumeration (protostar through whiteDwarfOrRemnant), so the present module supplies its own canonical list for the J-cost analysis.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. The tactic exhausts the Fintype instance generated by the five constructors of StellarPhase and confirms the resulting cardinality equals 5.
why it matters
The result supplies the five_phases field of the downstream stellarEvolutionCert definition, which packages the phase count into a certificate for stellar evolution models. It directly instantiates the module claim that phase count equals configDim D=5 under the J-cost framework. The declaration closes a finite enumeration step linking the Recognition Composition Law and phi-ladder to observable astrophysical stages, with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.