echoDelay_pos
plain-language theorem explainer
The theorem establishes that the echo delay Δt(N) is strictly positive for every natural number rung N. Gravitational-wave echo cataloguers and black-hole ringdown analysts cite it when certifying positivity of RS-derived delays. The proof is a term-mode reduction that unfolds the definition and chains mul_pos with bounceRadius_pos and Real.log_pos one_lt_phi.
Claim. For every natural number $N$, the echo delay satisfies $0 < 2 r_0(N) log φ$, where $r_0(N)$ is the bounce radius at rung $N$.
background
In the Recognition Science treatment of strong-field quantum gravity the bounce radius is $r_0(N) = φ^{N/2}$ (Planck units) and the echo delay is defined by $Δt(N) = 2 r_0(N) log φ$. This supplies the positivity ingredient required by the BlackHoleEchoesCert structure. The upstream lemma one_lt_phi states $1 < φ$, which forces $log φ > 0$.
proof idea
Term-mode proof: unfold echoDelay, then apply mul_pos (mul_pos (by norm_num) (bounceRadius_pos N)) and close with exact Real.log_pos one_lt_phi.
why it matters
The result populates the echo_delay_pos slot of bhEchoesCert and blackHoleEchoesCert, which in turn feed black_hole_echoes_one_statement. It thereby completes the positivity half of the RS black-hole echo predictions, linking the phi-ladder (T5–T6) to observable gravitational-wave delays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.