GalaxyMorphology
plain-language theorem explainer
The inductive type enumerates the five Hubble galaxy morphologies as an enumeration tied to configDim D = 5. An astrophysicist formalizing morphology counts in Recognition Science would cite this enumeration when establishing finite-type cardinality. The declaration is a direct inductive definition with five constructors and automatic derivation of Fintype together with decidable equality.
Claim. Let $G$ be the inductive type whose constructors are elliptical, lenticular, spiral, barred spiral, and irregular. The type is equipped with decidable equality, a representation, boolean equality, and finite cardinality.
background
The module introduces five canonical Hubble-sequence morphology types set equal to the configuration dimension parameter D = 5. These are the standard morphological classes used in the Recognition Science treatment of astrophysical structure. No upstream results are invoked; the declaration stands as a base enumeration.
proof idea
The declaration is the inductive definition itself, introducing the five constructors directly and deriving the type classes DecidableEq, Repr, BEq, and Fintype by the deriving clause.
why it matters
This enumeration is the input required by the downstream structure GalaxyMorphologyCert, which records that the finite cardinality equals 5, and by the theorem galaxyMorphology_count proved by decision. It supplies the concrete set whose size matches the configDim D = 5 convention stated in the module, placing the morphology count inside the Recognition framework that derives spatial dimension D = 3 and the eight-tick octave from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.