BHEchoesCert
plain-language theorem explainer
BHEchoesCert packages four field properties that certify strict positivity and exact phi scaling for bounce radii and echo delays at every recognition rung. Gravitational-wave modelers cite it when mapping LIGO/Virgo catalog events to RS bounce predictions. The definition is a direct bundling of the four lemmas already established for bounceRadius and echoDelay in the same module.
Claim. A structure $B$ such that $r(N) > 0$ for all $N$, $r(N+1) = r(N)·ϕ$ for all $N$, $Δt(N) > 0$ whenever $N ≥ 1$, and $Δt(N+1) = Δt(N)·ϕ$ whenever $N ≥ 1$, where $r(N) := ϕ^N$ is the bounce radius at rung $N$ and $Δt(N) := 2 r(N) log ϕ$ is the corresponding echo delay.
background
In Recognition Science the bounce radius at rung $N$ is defined by $r(N) := ϕ^N$ (RS-native units). The echo delay follows as $Δt(N) := 2 r(N) log ϕ$, the geometric round-trip multiplier from the bounce surface. Module BHEchoesLIGOCatalog assembles these into a certificate for LIGO/Virgo events, resting on the geodesic-completeness result that guarantees positivity at every rung.
proof idea
One-line structure definition that directly collects the four lemmas bounceRadius_pos, bounceRadius_succ_ratio, echoDelay_pos and echoDelay_succ_ratio already proved for the sibling definitions bounceRadius and echoDelay.
why it matters
BHEchoesCert supplies the structural certificate required by the downstream bhEchoesCert definition, which populates the catalog of events for which the RS bounce-echo prediction is permitted. It implements the per-event delay positivity and rung-to-rung ratio demanded by the module's headline events (GW150914, GW170817, GW190521, GW230529). In the framework this closes the link from T5 J-uniqueness and T6 phi fixed point to observable gravitational-wave signatures, with null results on high-SNR events serving as a potential falsifier of the bounce mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.