echoDelay_pos
plain-language theorem explainer
echoDelay_pos establishes that the RS-predicted gravitational wave echo delay remains strictly positive whenever the bounce radius r_min exceeds zero. Black-hole ringdown analysts and LIGO echo cataloguers cite it to certify that all predicted delays are observable. The proof is a one-line wrapper applying mul_pos to the three positive factors 2, r_min and log phi.
Claim. If $0 < r_ {min}$, then $0 < 2 r_{min} log phi$.
background
In the Recognition Science treatment of strong-field black-hole echoes the delay is defined by echoDelay r_min := 2 r_min rungPhaseDelay, where rungPhaseDelay equals Real.log phi. The module GravitationalWaveEchoFromRS imports this definition from BlackHoleEchoesFromBounce together with the constant phi from Constants. Upstream, one_lt_phi proves 1 < phi by comparing sqrt(5) to 2, which immediately yields log phi > 0 via Real.log_pos.
proof idea
The proof is a one-line wrapper that applies mul_pos (mul_pos (by norm_num) hr) (Real.log_pos one_lt_phi). It chains the positivity of the constant 2, the hypothesis 0 < r_min, and the fact that log phi > 0 supplied by one_lt_phi.
why it matters
The theorem supplies the echo_delay_pos field required by bhEchoesCert and blackHoleEchoesCert, and is invoked inside gwEchoCert and black_hole_echoes_one_statement. It closes the positivity link in the echo train whose amplitude damps by 1/phi per echo, consistent with the five-parameter echo set matching configDim D = 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.