HeadlineEvent
plain-language theorem explainer
HeadlineEvent enumerates the four canonical LIGO/Virgo events (GW150914, GW170817, GW190521, GW230529) that anchor per-event black-hole echo predictions in the Recognition Science catalog. Gravitational-wave analysts working on echo searches cite this finite list when assigning recognition rungs and computing echo delays from the phi-ladder. The declaration is a plain inductive type with four constructors that automatically derives decidable equality and Fintype structure.
Claim. Let $E$ be the inductive type whose four constructors are the events GW150914, GW170817, GW190521 and GW230529.
background
The module Gravity.BHEchoPerEventCatalog records per-event tables that complement the generic structural BH-echo cert. For each event it supplies a recognition rung $N$ obtained from log-mass scaling, the predicted bounce radius, echo delay $Δt(N)$ and echo frequency $f_{echo}(N)=1/Δt(N)$ in RS-native units. The supplied table lists the four events with their approximate masses and assigned rungs (8, 1, 10, 2). Upstream rung definitions appear in Compat.Constants, AsteroidOreSpectroscopy, AnchorPolicy and RSBridge.Anchor; these supply the integer-valued rung map used to index the phi-ladder predictions.
proof idea
Inductive definition with four explicit constructors. Derives DecidableEq, Repr, BEq and Fintype by the deriving clause; no tactics or lemmas are applied.
why it matters
HeadlineEvent supplies the finite domain for BHEchoCatalogCert, which asserts that the catalog contains exactly four events and that all predicted bounce radii, delays and frequencies are strictly positive. It feeds catalogAmplitude and the per-event functions predictedBounceRadius, predictedEchoDelay and predictedEchoFrequency. The construction closes the per-event falsification path described in the module doc: any high-SNR event whose echo signature fails to appear at the predicted rung falsifies the catalog. It sits inside the gravity sector that applies the Recognition Composition Law and the eight-tick octave to black-hole echoes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.