pith. machine review for the scientific record. sign in
def definition def or abbrev high

bounceRadius

show as:
view Lean formalization →

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 in Recognition Science

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$.

scope and limits

formal statement (Lean)

  35noncomputable def bounceRadius (N : ℕ) : ℝ := phi ^ N

proof body

Definition body.

  36

used by (19)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.