echoDelay_pos
plain-language theorem explainer
The theorem establishes that the echo delay at recognition rung N remains strictly positive for every N at least 1. Gravitational-wave analysts comparing LIGO/Virgo ringdown signals to bounce-echo predictions would cite this result to confirm that every catalog event carries a positive predicted delay. The proof unfolds the echoDelay definition, obtains log phi greater than zero from the bound phi greater than 1.5, pulls in the already-proved positivity of bounceRadius N, and closes with the positivity tactic.
Claim. For every natural number $N$ with $Ngeq 1$, the echo delay $Delta t(N)=2cdot phi^Ncdotlogphi$ satisfies $Delta t(N)>0$.
background
The module develops black-hole echo predictions for the LIGO/Virgo catalog. The geodesic-completeness theorem supplies the recognition-lattice bounce radius $r_min(N)=phi^N$ (in RS-native units) and the echo delay $Delta t(N)=2 r_min log phi$, both required to be strictly positive for every rung $Ngeq 1$. This positivity result is one of the four components of the BHEchoesCert structure that certifies the catalog. Constants.phi_gt_onePointFive supplies the tighter lower bound phi greater than 1.5, which immediately yields log phi greater than zero via the real logarithm positivity lemma.
proof idea
The proof unfolds the definition of echoDelay, obtains phi greater than 1.5 from Constants.phi_gt_onePointFive and closes the inequality with linarith, deduces 0 less than log phi via Real.log_pos, invokes bounceRadius_pos N to obtain 0 less than bounceRadius N, and finishes with the positivity tactic.
why it matters
This theorem supplies the echo_delay_pos field of the bhEchoesCert certificate and is used by predictedEchoDelay_pos to verify positivity for each headline event. It also appears in the BlackHoleEchoesCert structure and the one-statement black-hole-echoes theorem. Within the Recognition Science framework it closes the positivity requirement for the bounce-echo mechanism at every rung, consistent with the phi-ladder scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.