GWSourceCategory
plain-language theorem explainer
GWSourceCategory enumerates the five canonical gravitational wave source classes in Recognition Science astrophysics. Binary merger modelers cite it when mapping mass classes to the phi-decay law for strain ratios. The declaration is a direct inductive type equipped with decidable equality and finite-type structure.
Claim. The inductive type of gravitational wave source categories consists of the five constructors: neutron-star--neutron-star, black-hole--neutron-star, black-hole--black-hole, supermassive black hole, and stochastic background.
background
In the module on gravitational wave amplitude from J-cost, strain for binary mergers satisfies h proportional to M^{5/3} over distance. Recognition Science expresses the ratio of strains between adjacent mass classes via the phi-decay law. The local setting introduces five canonical source categories that realize config dimension D = 5, with the prediction that adjacent classes differ in peak strain by phi.
proof idea
This is a direct inductive definition that introduces five constructors and derives instances for decidable equality, representation, boolean equality, and finite type.
why it matters
The enumeration supplies the finite set required by GravitationalWaveCert, which asserts cardinality 5 together with the phi-ratio property for strains at successive rungs. It realizes config dimension D = 5 for astrophysical sources, extending the phi-ladder from particle masses to gravitational wave amplitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.