galaxyMorphologyCert
plain-language theorem explainer
The definition constructs the certificate asserting exactly five galaxy morphology types in the Hubble sequence, aligned with configuration dimension five. Astrophysicists applying discrete classification in Recognition Science models would cite it when invoking the five-type taxonomy. Construction is a direct structure instantiation that supplies the value from the decidable cardinality theorem.
Claim. The structure certifying that the finite type of galaxy morphologies has cardinality $5$, instantiated by supplying the value from the theorem establishing that cardinality.
background
The module establishes five canonical Hubble-sequence morphology types (elliptical, lenticular, spiral, barred spiral, irregular) as the discrete set whose count equals configuration dimension D = 5. GalaxyMorphologyCert is the structure whose sole field requires that the cardinality of this finite type equals five. The upstream theorem proves the cardinality equality by a decision procedure and is referenced directly to populate the certificate.
proof idea
One-line wrapper that applies the cardinality theorem to fill the five_types field of the certificate structure.
why it matters
This supplies the certified count of five morphology types required by the astrophysics layer of the Recognition Science framework, where configDim fixes the discrete classification. It closes the local derivation of Hubble types from D = 5 and stands ready for any larger galaxy modeling that invokes the morphology taxonomy. No downstream theorems are listed, leaving it as a terminal certificate in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.