BHEchoCatalogCert
plain-language theorem explainer
BHEchoCatalogCert packages the per-event BH-echo predictions for the four headline LIGO/Virgo events by requiring a catalog size of four, strict positivity of bounce radii, delays and frequencies, and the rung ordering GW170817 < GW230529 < GW150914 < GW190521. Gravitational-wave modelers working in Recognition Science cite it when tabulating echo signatures against observed masses. The declaration is a plain structure definition that directly assembles these properties from the module's sibling definitions.
Claim. Let $E$ be the finite set of headline events with $|E|=4$. The catalog certificate asserts that the predicted bounce radius $r_b(e)>0$, echo delay $Δt(e)>0$ and echo frequency $f(e)>0$ for every $e∈E$, together with the strict rung ordering $N(GW170817)<N(GW230529)<N(GW150914)<N(GW190521)$, where $N$ is the recognition rung assigned by log-mass scaling.
background
HeadlineEvent is the inductive type enumerating the four canonical LIGO/Virgo events GW150914, GW170817, GW190521 and GW230529. predictedRung, predictedBounceRadius, predictedEchoDelay and predictedEchoFrequency are the module's per-event functions that lift the generic bounceRadius and echoDelay scalings to each named event. The module records the explicit per-event table in RS-native units, with rung $N$ chosen from log-mass scaling and adjacent-rung frequencies related by the factor $1/φ$.
proof idea
This is a structure definition with no proof body. The fields are filled by direct reference to the sibling theorems event_count, predictedBounceRadius_pos, predictedEchoDelay_pos, predictedEchoFrequency_pos and rung_ordering.
why it matters
The structure supplies the concrete per-event certificate that is instantiated by bhEchoCatalogCert. It completes the catalog side of the BH-echo prediction framework, allowing direct comparison of predicted echo delays and frequencies against LIGO data. The rung ordering and positivity conditions implement the falsifiability criterion stated in the module: any high-SNR event whose echo signature fails to appear at the predicted rung refutes the catalog.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.