starFormationCert
plain-language theorem explainer
The starFormationCert definition assembles a certificate for star formation in Recognition Science by confirming five evolutionary stages and a phi-based Jeans mass ratio across density rungs. Astrophysicists modeling molecular cloud collapse under RS would reference this to link the phi-ladder to observed stellar evolution phases. It is constructed directly by substituting the stage count theorem and the mass ratio theorem into the StarFormationCert structure.
Claim. The declaration defines a certificate for the star formation process asserting that stellar evolution occurs through five stages and that the Jeans mass at successive rungs on the density ladder satisfies $M_J(k+1)/M_J(k) = phi$ for every natural number $k$.
background
In the Recognition Science treatment of astrophysics, star formation proceeds via collapse of molecular clouds whose densities follow the phi-ladder. The module identifies five canonical stages: molecular cloud, prestellar core, protostar, T Tauri star, and main sequence, corresponding to a configuration dimension of 5. The Jeans mass at each rung scales according to the golden ratio phi. The upstream theorem starFormationStageCount establishes that the finite type of StarFormationStage has cardinality 5. The theorem jeansMassRatio shows that the ratio of Jeans masses at consecutive rungs equals phi by unfolding the mass definition and applying algebraic simplification with positivity of phi.
proof idea
The definition constructs the StarFormationCert structure by setting the five_stages field to the theorem starFormationStageCount and the phi_ratio field to the theorem jeansMassRatio. It is a direct record construction with no additional computation.
why it matters
This definition furnishes the explicit certificate required by the StarFormationCert structure in the star formation module. It ties the five-stage sequence and the phi-scaled Jeans masses to the broader RS framework, where the phi-ladder governs mass formulas and the golden ratio appears as the self-similar fixed point. The module documentation positions this as part of deriving stellar evolution from RS principles, though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.