gwSourceCount
plain-language theorem explainer
Five gravitational wave source categories are enumerated in the Recognition Science treatment of interferometry. Researchers classifying LIGO events reference the cardinality to set the configuration dimension. The equality follows from a direct computation on the finite inductive definition of the source type.
Claim. $ | { BH-BH merger, NS-NS merger, BH-NS merger, continuous wave, stochastic background } | = 5 $
background
The module identifies gravitational wave strain with the J-cost of metric perturbations. It introduces the inductive type GWSourceType whose constructors are BHBH, NSNS, BHNS, continuousWave and stochastic. This fixes the number of source classes at five, matching the configuration dimension in the Recognition Science framework. The upstream theorem in Astrophysics.GravitationalWaveFromJCost establishes the same cardinality for a related category type.
proof idea
The proof applies the decide tactic to the cardinality equality. Since GWSourceType derives Fintype, the tactic evaluates the finite enumeration and confirms the count equals five.
why it matters
The theorem populates the five_sources field in gwInterferometryCert and the five_categories field in gravitationalWaveCert. It supplies the discrete source count required for the interferometry certificate, which in turn supports the J-cost based strain threshold. This step anchors the gravitational wave modeling to the five-type classification within the Recognition Science derivation of physics constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.