GWSourceType
plain-language theorem explainer
GWSourceType enumerates the five canonical gravitational wave source classes in the J-cost framework: binary black hole mergers, neutron star mergers, black hole-neutron star mergers, continuous waves, and stochastic backgrounds. A physicist mapping LIGO/Virgo strain data to Recognition Science metric perturbations would cite this enumeration when classifying signals. The declaration is a direct inductive definition whose Fintype instance is generated automatically to support downstream cardinality claims.
Claim. The set of gravitational wave source types is the inductive type with five constructors: binary black hole merger (BHBH), neutron star-neutron star merger (NSNS), black hole-neutron star merger (BHNS), continuous wave, and stochastic background, equipped with decidable equality and finite type structure.
background
The module treats LIGO/Virgo sensitivity of order 10^{-21} strain at 100 Hz as the J-cost of metric perturbations, with detection threshold J(r) < J(φ) for J(φ) in (0.11, 0.13). Five canonical source types are identified with configDim D = 5. The imported CanonicalJBand supplies the J functional equation whose values label these source classes. The inductive definition supplies the finite set whose cardinality is later asserted to be five.
proof idea
This is a direct inductive definition with five constructors. The deriving clause for DecidableEq, Repr, BEq, and Fintype is automatic; no explicit proof body is required. The Fintype instance is used immediately by the sibling theorem that computes the cardinality via decide.
why it matters
The definition supplies the source enumeration required by the GWInterferometryCert structure, which records both Fintype.card GWSourceType = 5 and the CanonicalCert for the detection threshold. It realizes the configDim D = 5 assignment stated in the module, connecting the J-cost equation to the discrete channels of gravitational wave interferometry. The five types provide the configuration space whose cardinality is discharged in the downstream gwSourceCount theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.