BHEchoAmplitudeCert
plain-language theorem explainer
BHEchoAmplitudeCert bundles the positivity, unit primary value, and successive phi^{-1} damping properties of the echo amplitude function into one certificate object. Gravitational-wave analysts searching LIGO merger data for post-bounce reflections would cite it to test the predicted SNR ratio of 1/phi between successive echoes. The structure is assembled by direct reference to the six sibling lemmas that establish each field.
Claim. A structure asserting that the echo amplitude function satisfies $A(n)>0$ for all $n$, $A(0)=1$, $A(n+1)=A(n)·φ^{-1}$, $A(n+1)/A(n)=φ^{-1}$, $A(n+1)<A(n)$, and that the catalog amplitudes $A_e(n)$ for each HeadlineEvent $e$ are likewise positive.
background
The module treats black-hole echoes as successive reflections off a bounce surface, each incurring one rung of phi-ladder recognition cost. This yields the explicit form echoAmplitude n := phi^(-n), with catalogAmplitude simply forwarding the same function for each of the four HeadlineEvent constructors (GW150914, GW170817, GW190521, GW230529). The upstream echoAmplitude definition in GravitationalWaveEchoFromRS supplies the same phi-power expression, while the per-event catalog supplies the event enumeration.
proof idea
This is a structure definition whose six fields are filled by naming the pre-proven sibling lemmas echoAmplitude_pos, echoAmplitude_one, echoAmplitude_succ_ratio, echo_snr_ratio, echoAmplitude_strictly_decreasing, and catalogAmplitude_pos. No further reduction or tactic is applied.
why it matters
The certificate supplies the amplitude half of the echo prediction and is instantiated by the downstream bhEchoAmplitudeCert. It realizes the phi-ladder damping rule stated in the module documentation, where each reflection multiplies amplitude by phi^{-1} and produces the constant SNR ratio 1/phi. This connects to the Recognition Science self-similar fixed point phi and supplies a concrete falsifiable signature for gravitational-wave searches that compounds with the delay catalog from BHEchoPerEventCatalog.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.