predictedEchoFrequency_pos
plain-language theorem explainer
The theorem shows that the predicted echo frequency remains strictly positive for each of the four canonical LIGO/Virgo headline events. Workers certifying black-hole echo tables in Recognition Science or modified-gravity models cite it to close the positivity column of the catalog. The proof is a one-line term that unfolds the reciprocal definition and feeds the already-proved delay positivity into div_pos.
Claim. For every headline event $e$, the predicted echo frequency satisfies $0 < 1/Δt(e)$, where $Δt(e)$ is the echo delay determined by the recognition rung of $e$.
background
The module supplies per-event tables for the four headline LIGO/Virgo events (GW150914, GW170817, GW190521, GW230529). Each event carries a recognition rung $N$ obtained from log-mass scaling; the echo delay $Δt(N)$ is a positive multiple of powers of $φ$ and $log φ$ in RS-native units, and the echo frequency is defined as its reciprocal. The upstream theorem predictedEchoDelay_pos already establishes $0 < Δt(e)$ for every headline event by exhaustive case analysis on the inductive HeadlineEvent type together with echoDelay_pos.
proof idea
The term proof first unfolds the definition of predictedEchoFrequency, exposing the division $1 / predictedEchoDelay e$. It then applies the lemma div_pos to the positivity of one and the result of predictedEchoDelay_pos e.
why it matters
The result is collected inside the bhEchoCatalogCert definition, which bundles bounce-radius positivity, delay positivity, frequency positivity and rung ordering into a single certificate. This certificate supports the structural BH-echo cert in the Gravity section and confirms that all catalog frequencies lie on the positive phi-ladder, consistent with the eight-tick octave and D=3 framework landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.