GWSourcesCert
plain-language theorem explainer
GWSourcesCert defines a structure that certifies the inductive type of gravitational wave source classes has cardinality exactly five. Modelers of gravitational wave signals in Recognition Science would cite it to fix the source taxonomy dimension at configDim D=5. The declaration is a direct structure with one field recording the Fintype cardinality of GWSourceClass.
Claim. The structure $GWSourcesCert$ is defined by the single field asserting that the cardinality of the set of gravitational wave source classes equals five, i.e., $|GWSourceClass|=5$, where $GWSourceClass$ enumerates the five classes compact binary, core collapse, continuous, stochastic background, and memory.
background
The module identifies five canonical gravitational wave source classes tied to configDim D=5: compact binary inspiral-merger-ringdown, core-collapse supernova, continuous emission from rotating neutron stars, stochastic background, and memory. These classes occupy distinct frequency bands from millihertz (LISA) to kilohertz (LIGO). The structure GWSourcesCert packages the assertion that this classification has Fintype cardinality five.
proof idea
The declaration is a structure definition introducing the type GWSourcesCert with the single field five_classes that records the equality Fintype.card GWSourceClass = 5. It depends only on the inductive definition of GWSourceClass and requires no tactics or lemmas beyond the structure declaration itself.
why it matters
This definition supplies the certificate instantiated by the downstream gwSourcesCert, which sets five_classes to the computed value from gwSourceClass_count. It anchors the source classification dimension at five inside the Recognition Science framework, matching the module's statement of zero sorry and zero axiom. The construction supports formal modeling of gravitational wave signals across the listed frequency bands.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.