echoDampingFactor_eq_reflectionAmplitude
plain-language theorem explainer
The per-trip echo damping factor equals the single-rung reflection amplitude; both are exactly $\varphi^{-1}$. Gravity and QG-echo workers cite this to identify geometric decay of successive echoes with barrier scattering. The proof is pure definitional equality (`rfl`).
Claim. The echo damping factor equals the single-rung reflection amplitude: both equal $\varphi^{-1}$.
background
In the near-horizon recognition model the barrier is $\varphi$-self-similar. At each rung the golden-ratio energy partition $1=\varphi^{-1}+\varphi^{-2}$ (equivalent to $\varphi^2=\varphi+1$) splits energy into reflected and transmitted parts. The reflected energy fraction is $\varphi^{-2}$, so the reflection amplitude is $|R|=\varphi^{-1}$.
The echo damping factor is defined as the multiplicative amplitude loss per successive echo trip, also $\varphi^{-1}$. The module records that echo $n$ therefore arrives with amplitude $\varphi^{-n}$ and delay $n\cdot\Delta t_{\mathrm{echo}}$. Both named quantities are plain real constants built from the RS constant $\varphi$.
proof idea
Both sides unfold to the same definition: the damping factor is $\varphi^{-1}$ and the reflection amplitude is $\varphi^{-1}$. The equality is therefore definitional and is discharged by rfl with no lemmas.
why it matters
This identity locks the geometric decay of gravitational-wave echoes to the barrier's scattering amplitude. The module's structural claim is that the QG-paper echo prediction is forced by $\varphi^2=\varphi+1$, not by dimensional analysis: the golden-ratio equation is the scattering matrix. Identifying damping with reflection amplitude makes that forcing explicit at the amplitude (not intensity) level. No downstream theorems currently depend on it; it is a local coherence fact inside the echo-coefficient development, sitting beside the partition completeness and positivity lemmas for the reflected/transmitted fractions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.