echoDelay_succ_ratio
plain-language theorem explainer
The echo delay satisfies Δt(N+1) = Δt(N) · φ for every integer N ≥ 1. Gravitational-wave modelers working with black-hole echo predictions from the Recognition Science bounce lattice would cite this scaling when propagating delays across catalog events. The proof is a one-line wrapper that unfolds the delay definition, rewrites via the adjacent-rung radius ratio, and closes by ring simplification.
Claim. For every integer $N$ with $N ≥ 1$, the echo delay obeys $Δt(N+1) = Δt(N) · φ$, where $Δt(N) := 2 · r_{min}(N) · log φ$ and $r_{min}(N)$ is the bounce radius at recognition rung $N$.
background
The module defines echo delay at rung $N$ by $Δt(N) = 2 · bounceRadius N · Real.log φ$, with bounceRadius itself given by the recognition-lattice expression $φ^{N/2}$. The local setting is the LIGO/Virgo catalog of events for which the geodesic-completeness bounce mechanism supplies a structurally permitted echo; the module proves positivity and adjacent-rung ratios for every $N ≥ 1$. The upstream bounceRadius_succ_ratio states that the bounce radius obeys the same scaling: adjacent-rung bounce-radius ratio = φ.
proof idea
The proof is a one-line wrapper that unfolds the echoDelay definition, rewrites using the bounceRadius_succ_ratio lemma, and simplifies the resulting algebraic expression with ring.
why it matters
The ratio is collected into the bhEchoesCert certificate that bundles all positivity and scaling facts for the LIGO catalog. It completes the per-rung delay scaling required by the geodesic-completeness theorem, ensuring that echo predictions remain consistent with the phi-ladder structure of the Recognition Science framework. The result directly supports the falsification test stated in the module: a null result on a high-SNR event with $N ≥ 1$ would falsify the RS bounce mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.