GWSourceClass
plain-language theorem explainer
Defines the inductive type of five gravitational wave source classes fixed by configDim equal to 5. Signal modelers working with LIGO and LISA data cite the enumeration when partitioning events by frequency band. The declaration is a bare inductive type that derives its Fintype instance automatically.
Claim. Let $C$ be the finite set of gravitational wave source classes. Then $C$ consists of the five elements compact binary, core collapse, continuous, stochastic background, and memory.
background
The module fixes configDim to 5 and enumerates the five canonical gravitational wave source classes that arise under this dimension. Each class occupies a distinct frequency interval running from millihertz scales accessible to LISA through kilohertz scales observed by LIGO. The inductive definition supplies the finite type whose cardinality is later asserted by the sibling theorem gwSourceClass_count.
proof idea
The declaration is an inductive definition that derives DecidableEq, Repr, BEq, and Fintype in a single line.
why it matters
The definition supplies the finite enumeration required by the downstream structure GWSourcesCert and the cardinality theorem gwSourceClass_count. It realizes the five source classes demanded by configDim equal to 5 inside the gravitational wave sector. No open questions or scaffolding remain attached to the declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.