StellarEvolutionCert
plain-language theorem explainer
The StellarEvolutionCert structure certifies that a stellar model has exactly five phases by requiring the finite type of StellarPhase to have cardinality five. Astrophysicists working with Recognition Science models of sun-like stars cite it to tie the configDim parameter to the observed sequence of protostar through remnant stages. The declaration is a bare structure definition that introduces the type with a single cardinality field and no further obligations.
Claim. A stellar evolution certificate is a structure asserting that the finite type of stellar phases has cardinality five, where the phases are the inductive enumeration consisting of protostar, main sequence, red giant branch, asymptotic giant branch, and white dwarf or remnant.
background
The module derives stellar evolution phases from the configDim parameter fixed at five for sun-like stars, listing the canonical sequence protostar, main sequence, red giant branch, asymptotic giant branch, and white dwarf or remnant. StellarPhase is the inductive type that enumerates these five stages and derives Fintype, DecidableEq, and related instances. This astrophysics-specific certificate is distinct from the upstream structure in Astronomy.StellarEvolutionFromJCost, which augments the same cardinality requirement with an additional CanonicalCert threshold field.
proof idea
The declaration is a structure definition that directly packages the single field five_phases : Fintype.card StellarPhase = 5. No lemmas are invoked and no tactics are used; the definition serves as a type-level wrapper whose only content is the cardinality assertion.
why it matters
This structure supplies the phase-count certificate consumed by the stellarEvolutionCert definitions in both the Astrophysics and Astronomy modules. It realizes the five-phase model required by configDim D = 5 and thereby connects the general forcing chain (T0-T8) to concrete stellar predictions. The definition closes the enumeration scaffolding for astrophysical applications of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.