bounceRadius_pos
plain-language theorem explainer
Bounce radius at every natural-number rung is strictly positive in RS-native units. LIGO echo modelers cite the result to guarantee that all predicted delays remain well-defined and positive. The proof is a term-mode one-liner that unfolds the definition and applies real-power positivity.
Claim. For every natural number $N$, $0 < r(N)$ where $r(N) = phi^N$ and $phi$ is the Recognition Science constant.
background
The BHEchoesLIGOCatalog module defines bounce radius at rung $N$ by the expression $phi^N$ in RS-native units. This sits inside the geodesic-completeness setting that assigns an integer rung gap to each black-hole merger and predicts an echo delay of the form $2 r(N) log phi$. The module imports Constants, which supplies the positivity of $phi$.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of bounceRadius to obtain $phi^N$ and then applies pow_pos instantiated with Constants.phi_pos.
why it matters
The theorem supplies the bounceRadius_pos field required by BHEchoesCert and by BlackHoleEchoesCert. It completes the positivity clause inside black_hole_echoes_one_statement, which collects the core RS bounce predictions for LIGO events. The result supports the falsifiability claim that a null echo detection on any high-SNR catalog event with rung at least one would refute the model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.