echoDelay
plain-language theorem explainer
Echo delay at recognition rung N is defined as twice the bounce radius at N multiplied by the natural log of phi. Gravitational wave researchers modeling black hole echoes in LIGO/Virgo catalogs would cite this when scaling delays for merger events. It is a direct definition that encodes the round-trip geometric factor from the bounce surface.
Claim. The echo delay at rung $N$ is $2 r_b(N) log phi$, where $r_b(N)$ is the bounce radius at that rung.
background
The Recognition Science framework derives bounce radius from the geodesic-completeness theorem as $phi^{N/2}$ in native units. Phi is the self-similar fixed point forced by J-uniqueness in the unified forcing chain. This module defines echo delay to catalog LIGO/Virgo events and prove per-event positivity and rung ratios.
proof idea
One-line definition that applies the round-trip multiplier 2 log phi directly to the bounce radius.
why it matters
This definition supplies the echo delay used in BHEchoesCert and black_hole_echoes_one_statement, which assert positivity and phi-scaling for echoes. It implements the catalog predictions for events such as GW150914 and connects to the phi-ladder and eight-tick octave in the forcing chain. Null results on high-SNR events with N >= 1 would falsify the bounce mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.