echoDelay
plain-language theorem explainer
The echo delay for a Recognition Science black-hole bounce at radius r_min is defined as twice the product of r_min and the per-rung phase delay log φ. Gravitational-wave analysts modeling LIGO ringdown echoes would cite this when testing the predicted φ-scaled delay train. It is a direct algebraic definition that composes the supplied radius with the logarithmic phase factor from the recognition lattice.
Claim. The echo delay satisfies $Δt(r_{min}) = 2 r_{min} log φ$, where $φ$ is the golden ratio fixed point of the recognition composition law.
background
In the Recognition Science treatment of black-hole interiors, collapse terminates at a finite bounce radius set by the rung gap traversed on the phi-ladder. The module assumes RS-native units with c = 1 and derives the two-way travel time for a wave packet to reach the bounce and return as an echo. The per-rung phase delay is log φ. This definition assembles the echo delay directly from that factor and the supplied r_min. It parallels similar echo delay constructions in the GravitationalWaveEchoFromRS and QuantumGravityFromRS modules.
proof idea
This declaration is a one-line definition that multiplies the radius argument by twice the per-rung phase delay.
why it matters
The definition supplies the core formula invoked in the BlackHoleEchoesCert structure to establish positivity and scaling relations for the echo train. It fills the structural identity for the echo signature in the module's theorem track, connecting to the phi fixed point and the eight-tick octave in the forcing chain. Downstream catalogs use it to predict delays for LIGO events, with the empirical echo signature serving as the falsifier at the observational level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.