predictedEchoDelay_pos
plain-language theorem explainer
The theorem establishes that the predicted echo delay for each of the four headline LIGO/Virgo events is strictly positive in RS-native units. Gravitational wave modelers using the Recognition Science black-hole echo catalog would cite this result to confirm all per-event time delays before deriving frequencies. The proof is a term-mode case split on the HeadlineEvent inductive type that reduces each constructor directly to the general echoDelay_pos lemma with a decide tactic for the rung bound.
Claim. For every headline event $e$, the predicted echo delay satisfies $0 < echoDelay(predictedRung(e))$, where echoDelay$(N)$ is the strictly positive function $Nmapsto bounceRadius(N)cdot log phi$ for rung $Ngeq 1$.
background
The module records per-event predictions for four canonical LIGO/Virgo events (GW150914 at rung 8, GW170817 at rung 1, GW190521 at rung 10, GW230529 at rung 2). Predicted echo delay is defined by applying the general echoDelay function to the event-specific predicted rung; the module table shows each delay scales as a positive multiple of log phi. This rests on the upstream echoDelay_pos theorem, which states that echo delay is strictly positive at every rung $Ngeq 1$ because both log phi and bounceRadius are positive.
proof idea
The proof unfolds predictedEchoDelay and predictedRung, performs case analysis on the four HeadlineEvent constructors, and applies echoDelay_pos to each case, discharging the lower bound $1leq N$ by the decide tactic.
why it matters
The result supplies the delay_pos field of the bhEchoCatalogCert definition, which aggregates event count, bounce-radius positivity, delay positivity, frequency positivity, and rung ordering into a single certificate. It directly supports the module's claim that the per-event ladder admits falsification by any high-SNR event whose echo signature fails to appear at the predicted rung. The positivity is required for the downstream frequency-positivity theorem and is consistent with the phi-ladder scaling used throughout the Recognition Science gravity catalog.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.