pith. sign in
module module high

IndisputableMonolith.Gravity.BHEchoPerEventCatalog

show as:
view Lean formalization →

This module enumerates the four canonical LIGO/Virgo headline events and equips each with rung assignments plus positive echo-delay formulas. Gravitational-wave analysts applying Recognition Science bounce models would cite it to instantiate the general catalog relations for specific mergers. The module consists entirely of definitions that specialize the upstream geodesic-completeness results to the named events.

claimThe module defines the finite catalog of headline events together with the maps predictedRung, predictedBounceRadius = φ^{N/2}, predictedEchoDelay = 2 φ^{N/2} log φ, and the associated positivity certificates for each event.

background

The upstream BHEchoesLIGOCatalog rests on the geodesic-completeness theorem, which supplies the recognition-lattice bounce radius r_min(N) = φ^{N/2} and echo delay Δt(N) = 2 r_min log φ, both strictly positive for N ≥ 1. This module names the four LIGO/Virgo headline events and instantiates those formulas per event. It introduces the HeadlineEvent predicate, rung_ordering, and BHEchoCatalogCert that certify the per-event delay positivity.

proof idea

This is a definition module, no proofs. It supplies named constants and functions that specialize the general bounce-echo formulas from the imported catalog module to the four headline events.

why it matters in Recognition Science

The module supplies the event-specific inputs required by the downstream BHEchoAmplitudes module, which attaches φ^{-1} damping to successive echo amplitudes. It thereby completes the per-event catalog step that feeds the structural SNR predictions for LIGO/Virgo data within the Recognition framework.

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)