bhEchoesCert
plain-language theorem explainer
The declaration assembles the BH echoes catalog certificate by supplying positivity and scaling proofs for bounce radii and echo delays. Gravitational-wave researchers would cite it when validating recognition-science bounce predictions against LIGO/Virgo catalog events. It proceeds as a direct structure instantiation using four upstream theorems on positivity and adjacent-rung ratios.
Claim. Let $r(N)$ denote the bounce radius at rung $N$ and let $t(N)$ denote the echo delay. The certificate asserts that $0 < r(N)$ for every natural number $N$, that $r(N+1) = r(N) phi$, that $0 < t(N)$ whenever $N >= 1$, and that $t(N+1) = t(N) phi$.
background
The module develops black-hole echo predictions for the LIGO/Virgo catalog. The geodesic-completeness theorem supplies the recognition-lattice bounce radius $r_min(N) = phi^{N/2}$ and echo delay $Delta t(N) = 2 r_min log phi$, both strictly positive for $N >= 1$. This certificate records that these quantities remain positive and scale by the golden ratio phi at adjacent rungs, enabling per-event checks for the four headline mergers (GW150914, GW170817, GW190521, GW230529).
proof idea
The definition is a direct record instantiation that assigns the four theorems bounceRadius_pos, bounceRadius_succ_ratio, echoDelay_pos, and echoDelay_succ_ratio to the fields of BHEchoesCert. Each assigned theorem unfolds the target function and applies either pow_pos on phi or the successor rule together with log_pos.
why it matters
This definition supplies the certificate required by the black-hole echoes module to certify structural permission for echo predictions on LIGO/Virgo events. It closes the catalog setup by confirming the positivity and phi-scaling properties that follow from the recognition composition law. No downstream uses are recorded, leaving open the integration of these delays into full waveform templates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.