GalaxyMorphologyCert
plain-language theorem explainer
The declaration defines a structure that certifies the finite set of galaxy morphology types has cardinality exactly five. Astrophysicists working with discrete Hubble-sequence classifications would cite it to fix the count of canonical types. It is realized directly as a structure whose single field records the cardinality fact derived from the inductive enumeration of the five classes.
Claim. Let $M$ be the finite set of galaxy morphology classes with elements elliptical, lenticular, spiral, barred spiral, and irregular. The structure asserts that the cardinality of $M$ equals 5.
background
The module fixes five canonical Hubble-sequence morphology types and equates this count to a configuration dimension of 5. These types are introduced via an inductive enumeration whose constructors are elliptical, lenticular, spiral, barred spiral, and irregular; the inductive definition automatically supplies a Fintype instance whose cardinality is therefore 5. This local convention sits inside the Recognition Science astrophysics layer and is independent of the spatial dimension D=3 obtained from the forcing chain T0-T8.
proof idea
The declaration is a structure definition containing one field. The field is populated by the cardinality computation that follows immediately from the five constructors of the inductive type; no separate lemma or tactic is required beyond the derived Fintype instance.
why it matters
The structure supplies the certified cardinality fact that the downstream definition galaxyMorphologyCert instantiates and exports. It thereby anchors the discrete morphology count of 5 inside the Recognition Science framework, consistent with the module's configDim=5 convention. This count supports higher-level galaxy morphology arguments without invoking the phi-ladder or the eight-tick octave directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.