StellarPhase
plain-language theorem explainer
The inductive definition enumerates five canonical phases of stellar evolution for sun-like stars under the Recognition Science parameterization by configDim equal to 5. Astrophysicists working with phase-count certificates would reference it to anchor the discrete stages protostar through remnant. The declaration is introduced directly as an inductive type that automatically derives the required decidable equality and finite-type instances.
Claim. The inductive type $StellarPhase$ is generated by the five constructors protostar, mainSequence, redGiantBranch, asymptoticGiantBranch, and whiteDwarfOrRemnant.
background
The module sets configDim to 5 to capture the five canonical stages of a sun-like star: protostar, main sequence, red giant branch, asymptotic giant branch, and white dwarf or supernova remnant. This local setting is stated explicitly in the module documentation and supplies the phase set required by the companion structure StellarEvolutionCert. The upstream inductive definition in Astronomy.StellarEvolutionFromJCost uses a different five-element partitioning (mainSequence, subgiant, redGiant, horizontalBranch, remnant) that likewise asserts cardinality 5 via a decide tactic.
proof idea
The declaration consists of the inductive definition itself together with the deriving clause for DecidableEq, Repr, BEq and Fintype. No separate proof body or tactic steps are present; the finite-type instance is obtained automatically from the five explicit constructors.
why it matters
The definition supplies the concrete phase enumeration demanded by the downstream StellarEvolutionCert structure, which records the equality Fintype.card StellarPhase = 5. It thereby closes the five-phase requirement tied to configDim D = 5 in the astrophysics layer of the framework and feeds the cardinality theorem stellarPhase_count proved by decide. No open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.