bounceRadius_pos
plain-language theorem explainer
Bounce radius defined as phi to the power of any natural number N is strictly positive. Black hole echo modelers in Recognition Science cite this to ensure the minimal radius stays positive for all rung values. The proof is a direct term application of the power positivity result for positive bases.
Claim. For every natural number $N$, the bounce radius $r(N) := phi^N$ satisfies $0 < r(N)$.
background
The Quantum Gravity from RS module supplies structural backing for the Planck-scale bounce in Recognition Science, where the bounce radius at recognition rung N is defined as phi raised to N in RS-native units. This supports the claim that r_min > 0 exists. Upstream definitions of bounceRadius appear in Gravity.BHEchoesLIGOCatalog and BlackHoleEchoesFromBounce as phi ^ N, with phi_pos establishing that the golden ratio exceeds zero.
proof idea
The proof is a one-line term proof that applies the lemma pow_pos to phi_pos and N.
why it matters
This result is referenced in the construction of bhEchoesCert and blackHoleEchoesCert, which certify black hole echo catalogs and predictions. It directly supports the requirement that the bounce radius remains positive, enabling downstream proofs of echo delay positivity and geometric amplitude decay by 1/phi. In the framework this aligns with the phi-ladder structure underlying the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.