StellarPhase
plain-language theorem explainer
StellarPhase enumerates the five canonical stages of stellar evolution in Recognition Science as main sequence, subgiant, red giant, horizontal branch, and remnant. Modelers of J-cost band crossings in astronomy cite this type to fix the phase set for cardinality and certification arguments. The declaration is a direct inductive enumeration that automatically derives Fintype for the subsequent count theorem.
Claim. Let $S$ be the finite set of stellar phases consisting of the five stages main sequence, subgiant, red giant, horizontal branch, and remnant, equipped with decidable equality and finite type structure.
background
In the Stellar Evolution from J-Cost module, stellar evolution proceeds by crossings of the canonical J(phi) band, where J denotes the recognition cost function J(x) = (x + x^{-1})/2 - 1. The module equates the number of phases to configDim D = 5. This inductive definition supplies the concrete phase labels used by downstream certification structures.
proof idea
The declaration is a direct inductive definition listing the five constructors, followed by automatic derivation of DecidableEq, Repr, BEq, and Fintype. No lemmas or tactics are invoked beyond the built-in inductive and deriving mechanisms.
why it matters
StellarPhase feeds the StellarEvolutionCert structure (five_phases : Fintype.card StellarPhase = 5 together with CanonicalCert) and the stellarPhaseCount theorem. It realizes the RS claim that five phases match config dimension 5 and phase transitions occur on the phi-ladder. The definition closes the interface between the J-cost model and the finite phase count required by the astronomy tier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.