Pith. sign in
module module moderate

IndisputableMonolith.Gravity.BHEchoesLIGOCatalog

show as:
view Lean formalization →

Structural BH-echo catalog in RS-native units: bounce radius and echo delay as functions of recognition rung N, with positivity and successive-rung ratio lemmas, bundled as a certificate. Per-event LIGO/Virgo prediction tables import these scalings. Mostly definitions plus elementary positivity and ratio proofs on the phi-ladder.

claimDefines bounce radius $R_b(N)$ and echo delay $\Delta t(N)$ at recognition rung $N$ (RS-native units), proves $R_b(N)>0$ and $\Delta t(N)>0$, records successive-rung ratios $R_b(N+1)/R_b(N)$ and $\Delta t(N+1)/\Delta t(N)$, and packages the structural claims in a black-hole echo certificate.

background

Recognition Science places mass and time scales on the discrete $\varphi$-ladder. A black-hole echo is modeled as a recognition bounce at rung $N$ outside the classical horizon, returning a delayed secondary pulse after the primary ringdown. Work is in RS-native units ($c=1$); the fundamental time quantum is $\tau_0=1$ tick from Constants.

This module supplies the generic structural maps $N\mapsto R_b(N)$ and $N\mapsto\Delta t(N)$, not event-specific numbers. Bounce radius is the radial scale tied to rung $N$; echo delay is the corresponding round-trip lag that sets the predicted echo time and frequency $f_{\mathrm{echo}}=1/\Delta t$.

proof idea

Definition-and-certificate module, not a deep existence proof. bounceRadius and echoDelay are introduced as rung-dependent quantities on the $\varphi$-ladder; positivity lemmas follow from positivity of the underlying constants and powers; successive-ratio lemmas are direct algebraic identities relating rung $N+1$ to $N$. BHEchoesCert / bhEchoesCert packages those facts into one structural certificate for importers.

why it matters in Recognition Science

Parent consumer is Gravity.BHEchoPerEventCatalog, which "gives the generic bounce-radius and echo-delay scaling" from this module and then "records the per-event prediction tables for the four canonical headline LIGO/Virgo events" (source mass $M$, rung $N$, $\Delta t(N)$, $f_{\mathrm{echo}}(N)=1/\Delta t(N)$). Bridges the discrete recognition ladder to concrete GW echo forecasts without reopening the T0–T8 forcing chain or the RCL derivation of $J$ and $\varphi$.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)