StarFormationStage
plain-language theorem explainer
The inductive type enumerates five canonical stages of star formation as molecular cloud, prestellar core, protostar, T Tauri, and main sequence. Astrophysicists applying the Recognition Science phi-ladder to cloud collapse would cite this enumeration to fix configDim D = 5 when counting stages or verifying mass ratios. The declaration is a direct inductive definition that derives Fintype to enable automatic cardinality proofs.
Claim. The star formation stages comprise the finite set consisting of the molecular cloud phase, the prestellar core phase, the protostar phase, the T Tauri phase, and the main sequence phase.
background
In the Recognition Science framework, stars form from molecular cloud collapse with formation rates governed by the phi-ladder of cloud density rungs. The module sets five canonical stellar evolution stages equal to configDim D = 5 and recalls the Jeans mass threshold M_J ∝ T^{3/2} ρ^{-1/2} scaled along the phi-ladder. This inductive definition supplies the explicit enumeration required for subsequent cardinality and ratio statements.
proof idea
The declaration is an inductive definition with five constructors that automatically derives DecidableEq, Repr, BEq, and Fintype instances. No separate proof body is needed; the Fintype derivation is supplied by the deriving clause.
why it matters
This definition supplies the five stages required by StarFormationCert to assert Fintype.card StarFormationStage = 5 together with the phi ratio for successive jeansMass values. It implements the configDim D = 5 step for astrophysics depth in the RS model and directly supports the downstream theorem starFormationStageCount. The construction links the phi-ladder mass formula to the five-stage sequence without invoking the eight-tick octave or spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.