module module high

`IndisputableMonolith.Gravity.BlackHoleEchoesFromBounce`

This module defines the RS bounce radius at rung gap N in Planck units, plus associated phase and echo delay quantities. Black hole information researchers cite these when modeling echoes from bounces inside the Recognition Science framework. The module supplies the core definitions and their basic positivity and monotonicity properties.

claimThe bounce radius $r_b(N)$ at rung gap $N$ is expressed in Planck length units and satisfies $r_b(N)>0$ with strict increase in $N$.

background

Recognition Science derives gravitational phenomena from the phi-ladder and J-cost functions on the eight-tick octave. This module sits in the gravity domain and imports the base time quantum τ₀ = 1 tick from the Constants module. It introduces bounceRadius as the RS bounce radius at rung gap N together with rungPhaseDelay and echoDelay, all scaled to Planck units.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed directly into the Black Hole Information Preservation module, which establishes the page curve and joint von Neumann entropy invariance to address the information paradox. They supply the concrete length and delay scales required for that theorem.

scope and limits

Does not derive the bounce radius from the forcing chain.
Does not compute numerical values for specific rung gaps.
Does not address non-RS or higher-dimensional gravity.

used by (1)

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

IndisputableMonolith.Gravity.BlackHoleInformationPreservation module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (22)

def bounceRadius L71
theorem bounceRadius_pos L73
theorem bounceRadius_zero L77
theorem bounceRadius_two_step L82
theorem bounceRadius_strict_mono L88
def rungPhaseDelay L99
theorem rungPhaseDelay_pos L101
theorem rungPhaseDelay_band L109
def echoDelay L134
theorem echoDelay_pos L136
theorem echoDelay_scaling L143
theorem echoDelay_two_step L149
def echoDampingRatio L159
theorem echoDampingRatio_pos L161
theorem echoDampingRatio_lt_one L165
theorem echoDampingRatio_band L170
def cumulativeEchoAmplitude L184
theorem cumulativeEchoAmplitude_pos L186
theorem cumulativeEchoAmplitude_strictly_decreasing L191
structure BlackHoleEchoesCert L202
def blackHoleEchoesCert L221
theorem black_hole_echoes_one_statement L241