module module high

`IndisputableMonolith.Gravity.BlackHoleEchoesFromBounce`

This module defines the RS bounce radius at rung gap N in Planck units, together with associated phase and echo delay quantities. Black-hole information researchers cite these when constructing echo models that preserve unitarity. It is a definition module containing no proofs.

claimThe RS bounce radius $r_b(N)$ at rung gap $N$, expressed in Planck units; together with rungPhaseDelay and echoDelay derived from it.

background

The module imports the Constants module whose sole documented object is the fundamental RS time quantum $\tau_0 = 1$ tick. Recognition Science models black-hole interiors via discrete rung ladders on the $\phi$-scale; the bounce radius supplies the length scale at which a collapsing configuration reflects rather than forming a classical singularity.

Sibling definitions establish positivity, monotonicity, and scaling properties of $r_b(N)$, rungPhaseDelay, and echoDelay. These quantities are expressed relative to the Planck length and are intended for insertion into entropy calculations.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions supply the geometric input required by the downstream BlackHoleInformationPreservation module, whose doc-comment states it tracks G1 of Plan v7 and proves the page curve together with joint von Neumann entropy invariance. The module therefore closes one link in the chain from RS bounce dynamics to resolution of the information paradox.

scope and limits

Does not derive the full Hawking evaporation spectrum.
Does not prove unitarity of the S-matrix.
Does not compute numerical echo times for concrete black-hole masses.
Does not address higher-dimensional or rotating cases.

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