starFormationStageCount
plain-language theorem explainer
The declaration fixes the number of star formation stages at five in the Recognition Science model of molecular cloud collapse. Astrophysicists citing the phi-ladder for stellar evolution would use this count to set the configuration dimension D equal to five. The proof is a one-line decision procedure that computes the cardinality from the automatically derived Fintype instance on the inductive enumeration of the stages.
Claim. The finite set of star formation stages has cardinality five, where the stages are the molecular cloud, prestellar core, protostar, T Tauri, and main sequence: $|S| = 5$ for $S = $ {molecular cloud, prestellar core, protostar, T Tauri, main sequence}.
background
The module treats star formation as collapse along the phi-ladder of cloud densities, with the rate governed by the Recognition Composition Law. The inductive type enumerates five stages: molecularCloud, prestellarCore, protostar, tTauri, mainSequence, each tied to a rung and equipped with a Fintype instance via the deriving clause. Module documentation states that these five stages realize configDim D = 5 and that the Jeans mass at rung k follows the phi-ladder scaling.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic evaluates the equality by enumerating the five constructors of the inductive type and confirming that the derived Fintype instance yields cardinality exactly five.
why it matters
The result populates the five_stages field of the downstream starFormationCert definition, which also carries the phi_ratio from the Jeans mass calculation. It supplies the explicit stage count required to embed the five-stage ladder into the Recognition Science framework, consistent with the module claim that star formation follows the phi-ladder and realizes D = 5. The declaration closes the finite enumeration needed before any further derivation of transition rates or mass thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.