StarFormationCert
plain-language theorem explainer
StarFormationCert is a structure that certifies exactly five stellar formation stages and constant phi scaling of Jeans mass across density rungs. Astrophysicists working in Recognition Science would cite it to anchor the phi-ladder model of molecular cloud collapse to the standard evolutionary sequence. The declaration is a bare structure definition whose two fields are populated directly from the Fintype instance on StarFormationStage and the exponential definition of jeansMass.
Claim. A certificate structure for Recognition Science star formation consisting of two fields: the cardinality of the set of stellar formation stages equals five, and for every natural number $k$ the ratio of Jeans masses at consecutive rungs satisfies $M_J(k+1)/M_J(k) = phi$.
background
In the Recognition Science treatment of astrophysics, star formation proceeds by collapse along a phi-ladder of molecular cloud densities. The five canonical stages are given by the inductive type StarFormationStage whose constructors are molecularCloud, prestellarCore, protostar, tTauri and mainSequence. The Jeans mass function is defined upstream as jeansMass(k) := phi^k, which directly encodes the self-similar scaling required by the Recognition Composition Law.
proof idea
The declaration is a structure definition with an empty proof body. It simply records the two certification properties: the Fintype.card equality for StarFormationStage and the universal ratio statement that follows immediately from the exponential form of jeansMass.
why it matters
StarFormationCert supplies the type for the concrete instance starFormationCert, which is built from starFormationStageCount and jeansMassRatio. It embeds the astrophysical application inside the Recognition Science framework by linking the phi-ladder (T6) to the five-dimensional configuration space of stellar evolution stages and thereby supports the rung-based mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.