bounceRadius
plain-language theorem explainer
Bounce radius at rung N is defined as phi raised to N in the reals. Black hole echo modelers working in Recognition Science cite it to obtain the scaling for delays and amplitudes from the bounce surface. The declaration is a direct power assignment that supplies the base quantity for subsequent positivity and ratio theorems.
Claim. $r_{min}(N) = phi^N$ in RS-native units for natural-number rung $N$, where $phi$ is the self-similar fixed point satisfying the Recognition Composition Law.
background
The Quantum Gravity from RS module states that the bounce radius satisfies $r_{min} = ell_{Planck} times phi^{N/2}$ for rung gap $N$. Upstream definitions in BlackHoleEchoesFromBounce and BHEchoesLIGOCatalog introduce the same quantity as $phi^N$ in RS-native units and pair it with the echo delay $Delta t(N) = 2 times bounceRadius(N) times log phi$. The module supplies structural backing for the Planck-scale bounce existing with $r_{min} > 0$, the echo delay being monotone in $N$, and the amplitude decaying geometrically by exactly $1/phi$ per echo.
proof idea
The declaration is a one-line definition that directly assigns the value $phi^N$.
why it matters
It supplies the core scaling quantity required by the BHEchoesCert structure for the bounce_radius_pos and bounce_radius_succ_ratio fields. The definition fills the A4 strong-field backing in the Quantum Gravity from RS module and connects to the phi-ladder scaling that appears in the forcing chain. It enables the echo-delay and amplitude calculations used in downstream LIGO-catalog predictions while supporting the claim that five canonical quantum-gravity approaches are subsumed under configDim $D=5$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.