bounceRadius_two_step
plain-language theorem explainer
The bounce radius function in RS-native units satisfies the scaling r(N+2) = r(N) * phi^2 for any natural number N. Gravitational-wave modelers analyzing black-hole ringdown echoes cite this identity to establish the geometric progression of bounce-induced delays across rung steps. The proof is a one-line wrapper that unfolds the definition of bounceRadius and applies the exponent addition rule.
Claim. For every natural number $N$, the bounce radius at rung $N+2$ equals the bounce radius at rung $N$ multiplied by $phi^2$, where the bounce radius at rung $N$ is defined as $phi^N$ in RS-native units.
background
In the Black-Hole Echoes from RS Bounce module the bounce radius is introduced as the scale at which J-cost divergence halts collapse, given explicitly by the definition bounceRadius(N) := phi^N (Planck length set to 1). This scaling arises from the phi-ladder forced by the self-similar fixed point in PhiForcingDerived and the dimensional structure in SpectralEmergence. The module works in RS-native units with c = 1 and focuses on structural identities for echo delays rather than empirical fitting.
proof idea
The proof is a one-line wrapper. It unfolds the definition of bounceRadius to obtain phi^(N+2), then rewrites via the power-addition lemma pow_add to factor the expression as phi^N * phi^2.
why it matters
This identity is collected inside the BlackHoleEchoesCert structure and directly supports the black_hole_echoes_one_statement theorem that packages all echo-train properties. It encodes the two-rung step on the phi-ladder, consistent with the self-similar fixed point phi from the UnifiedForcingChain. The result touches the open empirical question of whether LIGO/Virgo data exhibit the predicted phi-scaled echo delays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.