echoDelay_two_step
plain-language theorem explainer
The theorem states that the echo delay at bounce radius for rung N+2 equals the delay at rung N scaled by phi squared. Gravitational wave modelers analyzing RS bounce signatures in LIGO ringdown data would cite this scaling relation. The proof reduces the claim to the bounce radius two-step identity by unfolding the delay definition and applying algebraic normalization.
Claim. Let $r_N = phi^N$ denote the bounce radius at recognition rung $N$ in RS-native units, and let $Delta t(r) = 2 r cdot rungPhaseDelay$ be the echo delay for a given radius $r$, where rungPhaseDelay is the per-rung phase factor. Then $Delta t(r_{N+2}) = Delta t(r_N) cdot phi^2$.
background
In this module the bounce radius is defined by $r_min(N) = phi^N$ (Planck length set to 1). The echo delay is defined by $Delta t(r_min) = 2 r_min cdot rungPhaseDelay$, with rungPhaseDelay the constant per-rung phase delay on the recognition lattice. The module doc describes the setting: a nonsingular bounce at the Planck scale produces a delayed echo train in gravitational-wave ringdowns, with delay scaling as $2 r_min log phi$ (c = 1).
proof idea
The term-mode proof unfolds the echoDelay definition to expose its linear dependence on the radius argument. It then rewrites the radius argument via the upstream bounceRadius_two_step theorem, which supplies the exact factor phi^2. The ring tactic normalizes the resulting expression to obtain equality.
why it matters
The identity supplies the two-step scaling for echoDelay that is required by the BlackHoleEchoesCert structure and is packaged inside the black_hole_echoes_one_statement theorem. It instantiates the phi-ladder scaling (T6 fixed point, T7 eight-tick octave) for gravitational observables. The module treats the LIGO/Virgo echo signature as the empirical falsifier for the entire bounce model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.