galaxyMorphology_count
plain-language theorem explainer
The theorem asserts that the finite type of galaxy morphologies has cardinality five, matching the five Hubble-sequence classes. Astrophysicists using Recognition Science to fix configuration dimension at five would cite this result when certifying morphological counts. The proof is a one-line decision procedure that enumerates the five inductive constructors.
Claim. The cardinality of the finite type of galaxy morphology classes is five: $|GalaxyMorphology| = 5$.
background
The module introduces five canonical Hubble-sequence morphology types that realize configDim D = 5: elliptical, lenticular, spiral, barred spiral, irregular. These are encoded as the inductive type GalaxyMorphology whose five constructors derive DecidableEq, Repr, BEq and Fintype. The local setting is the Recognition Science treatment of galactic structure as a finite configuration space whose dimension is set by the underlying forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card computation on the inductive type GalaxyMorphology.
why it matters
This result supplies the cardinality field used by the downstream definition galaxyMorphologyCert. It directly implements the module claim that galaxy morphologies number five and thereby anchors the configDim = 5 choice inside the Recognition Science framework. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.