bounceRadius_zero
plain-language theorem explainer
The declaration proves that the RS bounce radius equals one Planck length at rung gap zero. Gravitational-wave modelers computing echo delays for minimal collapse gaps would cite this base case to initialize the phi-scaling ladder. The proof is a one-line wrapper that unfolds the bounceRadius definition and applies simplification to reduce phi to the power zero.
Claim. Let $r_0(N)$ denote the bounce radius at recognition rung gap $N$ in RS-native units with Planck length set to unity. Then $r_0(0) = 1$.
background
In the black-hole echo module the bounce radius is introduced as the function $r_0(N) = phi^N$ that replaces the classical singularity with a finite minimum set by the recognition rung gap traversed during collapse. The module works in RS-native units where $c=1$ and lengths are scaled to the Planck length, so the zero-gap case is the unit length. Upstream results supply the definition of phi as the self-similar fixed point and the rung function that indexes the recognition ladder.
proof idea
The proof is a one-line wrapper that unfolds the definition of bounceRadius and applies the simp tactic to evaluate phi to the power zero.
why it matters
This base case anchors the structural identities for bounce radius and echo delay in the black-hole echo module, which predicts phi-delayed signatures in LIGO/Virgo ringdowns. It corresponds to the zero rung in the phi-ladder of the Recognition framework and is consistent with the self-similar fixed point and eight-tick octave. The result is fully proved and closes the zero-gap instance of the scaling family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.