echoDelay_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute numerical delay values for concrete events.
- Does not address amplitude damping by 1/φ.
- Does not impose the side condition N ≥ 1.
- Does not derive monotonicity or two-rung scaling.
formal statement (Lean)
49theorem echoDelay_pos (N : ℕ) : 0 < echoDelay N := by
proof body
Term-mode proof.
50 unfold echoDelay
51 apply mul_pos (mul_pos (by norm_num) (bounceRadius_pos N))
52 exact Real.log_pos one_lt_phi
53