GWInterferometryCert
plain-language theorem explainer
The GWInterferometryCert structure asserts exactly five gravitational wave source types and requires the CanonicalCert for the detection threshold. Modelers of LIGO/Virgo sensitivity in Recognition Science terms cite it to equate source count with config dimension five and to enforce the phi-band strain limit. The declaration is a bare structure with two fields and no proof obligations.
Claim. A gravitational wave interferometry certificate consists of the statement that the finite type of source types has cardinality five together with an instance of the canonical J-band certificate for the detection threshold.
background
The module interprets LIGO strain sensitivity of order 10 to the minus 21 at 100 Hz as the J-cost of metric perturbations. Five source types are enumerated as black hole black hole mergers, neutron star neutron star mergers, black hole neutron star mergers, continuous waves, and stochastic backgrounds. The upstream CanonicalCert supplies the six clauses: matched zero at unity, reciprocity under inversion, positivity at phi, the open interval from 0.11 to 0.13 for J of phi, and positivity at the reciprocal of phi squared.
proof idea
The declaration is a structure definition that introduces the two fields five sources and detection threshold without any tactic steps or lemmas.
why it matters
This structure is instantiated by the downstream gwInterferometryCert definition to produce a concrete certificate. It realizes the module claim that five sources correspond to dimension five and that the detection threshold satisfies the phi band condition from the J-function. The construction grounds interferometry observables in the Recognition Science forcing chain via the J-cost and the eight tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.