gwSourcesCert
plain-language theorem explainer
The definition supplies a certificate fixing the number of gravitational wave source classes at five, matching the configuration dimension parameter. A physicist deriving emission models or detector response functions would cite it to lock the canonical set of five types spanning millihertz to kilohertz bands. Construction occurs by direct substitution of the upstream cardinality result into the certifying structure.
Claim. Let $GWSourcesCert$ be the structure whose sole field asserts that the finite type of gravitational wave source classes has cardinality five. The definition instantiates this structure by assigning the equality proved via decision procedure to that field.
background
The module treats gravitational wave sources as determined by the configuration dimension, which is set to five. This yields five canonical classes: compact binary inspiral-merger-ringdown, core-collapse supernova, continuous emission from rotating neutron stars, stochastic backgrounds, and memory effects. These classes occupy distinct frequency intervals from millihertz scales (LISA) to kilohertz scales (LIGO).
proof idea
The definition is a one-line wrapper that applies the cardinality theorem to populate the field of the certifying structure.
why it matters
This definition anchors the enumeration of gravitational wave source classes inside the physics module of Recognition Science. It supplies the concrete witness required for any downstream derivation that treats the configuration dimension as five, distinct from the spatial dimension three forced by the unified chain. No open questions are closed here, yet the step removes an enumeration hypothesis for source modeling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.