stellarPhase_count
plain-language theorem explainer
The theorem fixes the cardinality of the inductive StellarPhase type at five, matching the canonical phases for sun-like stars in the Recognition framework. Astrophysicists and modelers of stellar lifecycles cite this count to set configDim D equal to five. The proof is a direct decision computation that uses the derived Fintype instance on the five-constructor inductive definition.
Claim. The finite type of stellar evolution phases has cardinality five, consisting of the cases protostar, main sequence, red giant branch, asymptotic giant branch, and white dwarf or remnant.
background
The module introduces StellarPhase as an inductive type whose five constructors enumerate the standard evolutionary stages of a sun-like star. This construction sits inside the astrophysics layer and equates the phase count with configDim D = 5. An upstream inductive definition in Astronomy.StellarEvolutionFromJCost enumerates a related but distinct set of five phases (mainSequence, subgiant, redGiant, horizontalBranch, remnant) that supplies the J-cost foundation for the present enumeration.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic exploits the automatically derived DecidableEq, Repr, BEq, and Fintype instances on the inductive StellarPhase definition to evaluate the cardinality directly as five.
why it matters
The result populates the five_phases field inside the downstream stellarEvolutionCert definition, thereby certifying the phase count for the full stellar-evolution certificate. It implements the framework landmark that sets configDim D = 5 for stellar phases while remaining independent of the spatial dimension D = 3. The declaration closes a small explicit-count gap without introducing axioms or sorry placeholders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.