pith. sign in
module module high

IndisputableMonolith.Gravity.BHEchoAmplitudes

show as:
view Lean formalization →

The BHEchoAmplitudes module defines the echo amplitude at reflection number n relative to the primary signal. It augments the per-event BH echo catalog for four LIGO/Virgo events with amplitude scaling and supporting properties. The module consists of definitions together with positivity, normalization, ratio, and monotonicity lemmas.

claimLet $A(n)$ be the echo amplitude at reflection number $n$ (relative to the primary). Then $A(n)>0$ for all $n$, $A(1)=1$, the ratio $A(n+1)/A(n)$ satisfies a given recurrence, and $A(n)$ is strictly decreasing.

background

The module operates in the Gravity domain and imports BHEchoPerEventCatalog. That upstream module records per-event prediction tables for the four canonical LIGO/Virgo events, supplying source mass $M$, recognition rung $N$, echo delay $\Delta t(N)$ in RS-native units, and frequency $f_{\rm echo}(N)=1/\Delta t(N)$. Its doc states: "The structural BH-echo cert gives the generic bounce-radius and echo-delay scaling. This module records the per-event prediction tables." The present module adds the amplitude at each reflection.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the amplitude component that completes the per-event echo predictions. It feeds the BHEchoAmplitudeCert and bhEchoAmplitudeCert objects that certify amplitudes for the headline events, extending the structural scaling from the upstream catalog into quantitative signal strength.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)