module module moderate

`IndisputableMonolith.Gravity.BlackHoleEchoesSI`

SI packaging of black-hole bounce radius and exterior echo delay, built from Planck units and the φ-rung bounce algebra. Gravity workers who need RS echo times in seconds (for comparison with ringdown searches) cite these definitions. The module is mostly definitional: it composes the SI bridge with the quarantined rung formulas and records positivity and monotonicity.

claimDefines the SI Planck time $t_{\mathrm{P}}=\sqrt{\hbar_{\mathrm{SI}} G_{\mathrm{SI}}/c_{\mathrm{SI}}^{5}}$ and length $\ell_{\mathrm{P}}=c\,t_{\mathrm{P}}$, the SI bounce radius obtained by scaling the $\varphi$-rung bounce surface by $\ell_{\mathrm{P}}$, and the corresponding exterior echo delay in seconds, with positivity and strict monotonicity in the rung.

background

Recognition Science works in native units with $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$. The SI bridge closure supplies the unique calibration map that converts those native quantities into laboratory SI constants once a dimensional anchor is fixed.

Upstream, the black-hole echo module develops only the $\varphi$-rung algebra for bounce radius and echo delay. Its doc-comment is explicit: the physical bounce-to-exterior mechanism is not closed, and a true event horizon does not permit the earlier escape story. Only the rung algebra is treated as structural.

This module sits at the interface: it instantiates Planck time and length in SI, scales the bounce surface by $\ell_{\mathrm{P}}$, and exports echo delay in seconds so the gravity track can state predictions without leaving the formal development.

proof idea

Definition module with elementary lemmas, not a deep derivation. Planck time is the standard radical $\sqrt{\hbar G/c^{5}}$ in SI constants; Planck length is $c$ times that time. Positivity of both follows from positivity of the SI inputs. Bounce radius in SI is a two-step scaling of the upstream rung bounce surface by the Planck length; strict monotonicity in the rung is inherited from the dimensionless algebra. Echo delay in SI is the same conversion applied to the dimensionless delay. Square identities and the relation $\ell_{\mathrm{P}}=c,t_{\mathrm{P}}$ are short algebraic checks.

why it matters in Recognition Science

Feeds Gravity.MasterTheorem (Track 7.A), the conditional master statement that assembles the gravity track once its seven sub-tracks close. Without SI forms, echo-delay claims stay trapped in RS-native units and cannot be compared to ringdown timing. The module therefore closes the unit-facing half of the echo story while preserving the upstream quarantine: mechanism claims remain open; only the calibrated rung numbers are exported. It depends on the SI bridge closure (dimensional map) and on the bounce rung algebra (structural $\varphi$ identities only).

scope and limits

Does not assert a physical mechanism for waves escaping a true event horizon.
Does not close the bounce-to-exterior echo story quarantined upstream.
Does not derive new echo-delay numerics beyond SI packaging of the rung algebra.
Does not model detector response, selection effects, or observational bounds.
Does not alter RS-native constants; it only applies the SI calibration map.

used by (1)

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

IndisputableMonolith.Gravity.MasterTheorem module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.SIBridgeClosure module_import
IndisputableMonolith.Gravity.BlackHoleEchoesFromBounce module_import

declarations in this module (27)

def planckTime_SI L82
def planckLength_SI L85
theorem planckTime_SI_pos L87
theorem planckLength_SI_pos L92
theorem planckTime_SI_sq L98
theorem planckLength_SI_sq L105
theorem planckLength_SI_eq_planckTime_mul_c L112
def bounceRadius_SI L130
theorem bounceRadius_SI_pos L132
theorem bounceRadius_SI_two_step L136
theorem bounceRadius_SI_strict_mono L142
def echoDelay_SI L154
theorem echoDelay_SI_def L157
theorem echoDelay_SI_eq_planckTime_form L162
theorem echoDelay_SI_pos L169
theorem echoDelay_SI_two_step L177
theorem echoDelay_SI_strict_mono L183
theorem echoDelay_SI_sq L207
def echoDampingRatio_SI L224
theorem echoDampingRatio_SI_eq L226
theorem echoDampingRatio_SI_pos L228
theorem echoDampingRatio_SI_lt_one L231
theorem echoDampingRatio_SI_band L234
structure BlackHoleEchoesSICert L240
def blackHoleEchoesSICert L269
theorem blackHoleEchoesSICert_inhabited L286
theorem black_hole_echoes_SI_one_statement L294