pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Gravity.BHEchoAmplitudes

show as:
view Lean formalization →

This module defines the amplitude of black hole echoes at reflection number n relative to the primary signal and proves its basic properties. Analysts of LIGO/Virgo gravitational-wave data would cite it when quantifying echo strengths for the four headline events. The module consists of a core definition together with direct lemmas for positivity, normalization at n=1, successor ratio, and strict monotonic decrease.

claimLet $A(n)$ be the amplitude of the $n$th reflected echo relative to the primary. Then $A(1)=1$, $A(n)>0$ for all $n$, the ratio $A(n+1)/A(n)$ is constant and less than one, and $A(n)$ is strictly decreasing in $n$.

background

The module sits inside the Recognition Science gravity treatment and imports the per-event catalog from BHEchoPerEventCatalog. That catalog records, for each canonical LIGO/Virgo event, the source mass $M$, the recognition rung $N$, the predicted echo delay $Δt(N)$ in RS-native units, and the echo frequency $f_ echo(N)=1/Δt(N)$. The present module supplies the missing amplitude scaling that multiplies these delays to give observable signal strengths.

proof idea

This is a definition module. The central definition echoAmplitude is followed by one-line wrappers or direct algebraic checks establishing positivity, the base case at one, the constant successor ratio, and strict decrease.

why it matters in Recognition Science

The module completes the quantitative echo predictions begun in BHEchoPerEventCatalog by adding amplitude factors needed for signal-to-noise estimates. It therefore supplies the amplitude component required by any downstream comparison of Recognition Science forecasts against LIGO/Virgo strain data for the four headline events.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)