echoAmplitude
plain-language theorem explainer
The nth gravitational-wave echo carries relative amplitude φ^{-n}. GW-echo and near-horizon analyses cite this as the forced geometric decay from successive golden-ratio barrier reflections. It is a one-line definition: the single-rung reflection amplitude φ^{-1} raised to the echo index n.
Claim. For each natural number $n$, the relative amplitude of the $n$th gravitational-wave echo is $\varphi^{-n}$, where $\varphi$ denotes the golden ratio.
background
The module models the near-horizon recognition structure as a φ-self-similar potential barrier. At each rung boundary, energy splits by the golden-ratio partition $1 = \varphi^{-1} + \varphi^{-2}$, which is exactly $\varphi^2 = \varphi + 1$. The single-rung reflection coefficient is therefore $|R|^2 = \varphi^{-2}$, so the reflected amplitude is $|R| = \varphi^{-1}$.
Echo $n$ is the wave that has undergone $n$ such reflections. Its amplitude therefore decays geometrically as $\varphi^{-n}$, while the round-trip delay grows as $n \cdot \Delta t_{\mathrm{echo}}$ with $\Delta t_{\mathrm{echo}} = (\log\varphi)/(2\pi f_{\mathrm{ringdown}})$. Parallel definitions in BHEchoAmplitudes and GravitationalWaveEchoFromRS write the same quantity as $\varphi^{-n}$ (via integer powers or inverses), confirming a shared convention across the gravity stack.
proof idea
Pure definition: the body is the term $\varphi^{-1},^n$. No lemmas, tactics, or hypotheses are involved. Equivalent writings elsewhere use $\varphi^{-(n:\mathbb{Z})}$ or $(\varphi^n)^{-1}$; all three are definitionally the same real for $n\in\mathbb{N}$.
why it matters
This is the amplitude primitive for the entire BH-echo stack. BHEchoAmplitudeCert packages its positivity, unit primary ($n=0$), one-step ratio $\varphi^{-1}$, SNR ratio, and strict decrease. Downstream lemmas (echoAmplitude_pos, echoAmplitude_one, echoAmplitude_succ_ratio, echoAmplitude_strictly_decreasing, echo_snr_ratio) and catalogAmplitude for headline events all reduce to this power. In the Recognition framework the decay is not a fit: the module states that $|R|=\varphi^{-1}$ is forced by $\varphi^2=\varphi+1$, so the QG-paper echo prediction is a structural consequence of the φ-ladder barrier rather than dimensional analysis. It sits downstream of the T6 φ fixed-point and the self-similar rung structure that also underlies the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.