predictedEchoFrequency
plain-language theorem explainer
The definition assigns to each of the four headline LIGO/Virgo events its predicted echo frequency as the reciprocal of the corresponding echo delay. Gravitational-wave analysts comparing Recognition Science predictions against LIGO data would cite the resulting per-event frequencies. It is realized as a direct one-line reciprocal applied to the delay function.
Claim. For each headline event $e$, the predicted echo frequency is $f(e) := 1/Δt(N(e))$, where $N(e)$ is the recognition rung of $e$ and $Δt$ is the echo-delay function on the phi-ladder.
background
The module records per-event black-hole echo predictions for the four canonical LIGO/Virgo events enumerated by the inductive type HeadlineEvent. The echo delay for any such event is obtained by applying the echoDelay function to the predicted recognition rung of that event, which follows from log-mass scaling. The module doc states that each prediction satisfies $Δt > 0$ and $f > 0$ strictly, with adjacent-rung frequencies related by the factor $1/φ$.
proof idea
The definition is a one-line wrapper that applies the reciprocal operation to the output of predictedEchoDelay.
why it matters
This definition supplies the frequency-positivity clause inside the structure BHEchoCatalogCert and is invoked directly by the theorem predictedEchoFrequency_pos. It completes the per-event prediction table that links the recognition rung ladder to observable echo frequencies in the gravity sector. The construction uses the phi-ladder and eight-tick octave already fixed by the upstream forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.