gwSourceCount
plain-language theorem explainer
The declaration fixes the number of gravitational wave source categories at five in the Recognition Science model. Astrophysicists deriving strain ratios for binary mergers and stochastic backgrounds cite this count when building interferometry certificates. The proof is a direct decidable computation on the Fintype instance of the five-constructor inductive type.
Claim. The set of gravitational wave source categories has cardinality five: $|GWSourceCategory| = 5$.
background
The Astrophysics.GravitationalWaveFromJCost module treats gravitational wave strain as following a phi-decay law across mass classes, with adjacent binary merger categories differing in peak strain by the golden ratio. It introduces five canonical source categories (NS-NS, BH-NS, BH-BH, SMBH, stochastic) that realize configDim D = 5. The module documentation states: 'Five canonical GW source categories (NS-NS, BH-NS, BH-BH, SMBH, stochastic) = configDim D = 5.'
proof idea
The proof is a one-line wrapper that applies the decide tactic to the automatically derived Fintype instance on the inductive type GWSourceCategory whose five constructors are nsNS, bhNS, bhBH, smbh, and stochastic.
why it matters
This count populates the five_categories field of gravitationalWaveCert and the five_sources field of gwInterferometryCert. It supplies the concrete realization of configDim D = 5 from the forcing chain (T8) and the Recognition Composition Law setting. The module uses the result to anchor the RS prediction that adjacent source-class strains differ by phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.