echoDampingFactor
plain-language theorem explainer
The per-trip echo damping factor is fixed as the reciprocal of the golden ratio: each successive near-horizon echo multiplies amplitude by φ^{-1}. Gravity and QG-echo analyses cite it as the geometric decay constant of the φ-self-similar barrier. It is a one-line definition, not a derived inequality.
Claim. The echo damping factor is the real number $\varphi^{-1}$, so that each successive echo multiplies amplitude by one over the golden ratio.
background
The module treats 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 equivalent to $\varphi^2 = \varphi + 1$. The single-rung reflection coefficient is $|R|^2 = \varphi^{-2}$, so the reflected amplitude is $|R| = \varphi^{-1}$.
Echo $n$ is then assigned amplitude $\varphi^{-n}$ (geometric decay from $n$ rung reflections) and delay $n \cdot \Delta t_{\mathrm{echo}}$ with $\Delta t_{\mathrm{echo}} = (\log \varphi)/(2\pi f_{\mathrm{ringdown}})$. The constant $\varphi$ is the RS self-similar fixed point (forcing chain T6). Sibling defs in the module name the reflected and transmitted fractions and the reflection amplitude; this damping factor is the per-trip multiplier matching that amplitude.
proof idea
Pure definitional abbreviation: the real constant is set equal to $\varphi^{-1}$ from the Constants import. No tactics, no lemmas. Downstream equality with the reflection amplitude is reflexivity (rfl).
why it matters
Pins the geometric decay rate of black-hole (or horizon) echoes to the golden-ratio barrier without a free fit parameter. The module header states that $|R| = \varphi^{-1}$ is forced by $\varphi^2 = \varphi + 1$: the defining equation of φ is the barrier scattering matrix. Downstream, echoDampingFactor_eq_reflectionAmplitude records that this damping factor equals the reflection amplitude, and the next comment states that echo $n$ has amplitude proportional to $\varphi^{-n}$. That supplies the structural (not dimensional-analysis) echo prediction used in the QG paper track. Landmark link: T6 φ fixed point and the φ-ladder spacing of the recognition substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.