Pith. sign in
module module high

IndisputableMonolith.Gravity.BHEchoPerEventCatalog

show as:
view Lean formalization →

This module catalogs the four canonical LIGO/Virgo headline events and assigns recognition-lattice parameters for black-hole echo predictions. Gravitational-wave researchers testing bounce models would cite it for per-event rung and delay values. The module structure consists of event definitions together with positivity theorems for echo delays drawn from the upstream geodesic-completeness result.

claimThe catalog of four headline events, each equipped with rung $N$, bounce radius $r_{\min}(N)=\phi^{N/2}$, and echo delay $\Delta t(N)=2r_{\min}\log\phi$, all strictly positive for $N\ge1$.

background

The module resides in the Gravity domain and imports the LIGO catalog definitions. It rests on the geodesic-completeness theorem, which supplies the recognition-lattice bounce radius $r_{\min}(N)=\phi^{N/2}$ and echo delay $\Delta t(N)=2r_{\min}\log\phi$ for every $N\ge1$. The module enumerates the specific mergers for which these structural predictions are permitted and proves per-event positivity together with adjacent-rung ordering.

proof idea

The module first defines the headline events and their rung assignments, then applies the upstream delay formula to each event to obtain the positivity statements; the ordering theorem follows by direct comparison of the assigned rungs.

why it matters in Recognition Science

This module supplies the per-event echo delays and frequencies required by the amplitude predictions in BHEchoAmplitudes. It completes the catalog step that connects the geodesic-completeness theorem to concrete LIGO/Virgo observations within the black-hole echo chain.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)