predictedBounceRadius_pos
plain-language theorem explainer
The theorem establishes that the predicted bounce radius for each of the four canonical LIGO/Virgo headline events is strictly positive. Gravitational-wave analysts would cite it when confirming that all catalog entries meet the positivity requirement before comparing predicted echo frequencies to detector data. The proof is a one-line wrapper that invokes the general bounce-radius positivity result on the rung associated with the supplied event.
Claim. For every headline event $e$, the predicted bounce radius satisfies $0 < R_b(e)$, where $R_b(e)$ is the bounce radius obtained by applying the general bounce-radius function to the recognition rung of $e$.
background
The module records per-event predictions for black-hole echoes from the four headline LIGO/Virgo events (GW150914, GW170817, GW190521, GW230529). Each event carries a recognition rung $N$ chosen from logarithmic scaling of source mass in base phi; the predicted bounce radius is then the value of the general bounce-radius function at that rung. The local theoretical setting is the structural BH-echo certificate that supplies generic scaling for bounce radius and echo delay; this module specializes those scalings to the four events and tabulates the results in RS-native units, with every entry required to be strictly positive. An upstream theorem states that the bounce radius is strictly positive at every natural-number rung by unfolding its definition and invoking positivity of phi raised to that power.
proof idea
The proof is a one-line wrapper that applies the general bounce-radius positivity theorem to the (inferred) rung of the headline event.
why it matters
This theorem supplies the bounce_pos field inside the per-event BH-echo catalog certificate, which bundles positivity statements for radius, delay, and frequency together with rung ordering. It closes the positivity requirement for the catalog used in falsification tests of echo signatures at predicted rungs on the phi-ladder. The result sits inside the gravity domain and inherits the eight-tick octave structure from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.