echo_ratio_constant
plain-language theorem explainer
Successive black-hole echo amplitudes form a pure geometric series with fixed ratio φ^{-1}. Anyone citing the forced GW-echo reflection coefficient needs this identity. The proof is a short algebraic cancellation after unfolding the power-law amplitude definition.
Claim. For every natural number $n$, the ratio of successive echo amplitudes satisfies $A_{n+1}/A_n = \varphi^{-1}$, where $A_n = (\varphi^{-1})^n$.
background
The module treats the near-horizon recognition structure as a φ-self-similar potential barrier. Energy at each rung splits by the golden-ratio partition $1 = \varphi^{-1} + \varphi^{-2}$, which is exactly $\varphi^2 = \varphi + 1$. The single-rung reflection amplitude is therefore $|R| = \varphi^{-1}$, and the intensity is $|R|^2 = \varphi^{-2}$.
Locally, echo amplitude is defined by $A_n := (\varphi^{-1})^n$: the $n$-th echo has suffered $n$ rung reflections and decays geometrically. Equivalent definitions appear upstream as $\varphi^{-n}$ (integer exponent) in BHEchoAmplitudes and GravitationalWaveEchoFromRS; all three are the same real sequence.
The round-trip delay per rung is $(\log\varphi)/(2\pi f_{\mathrm{ringdown}})$. The present lemma isolates only the amplitude ratio, independent of timing.
proof idea
Term-mode algebraic reduction. Unfold $A_n = (\varphi^{-1})^n$. Rewrite the numerator via pow_succ as $(\varphi^{-1})^n\cdot\varphi^{-1}$. Commute the factors by a one-line ring identity, then cancel the common positive power $(\varphi^{-1})^n$ with mul_div_cancel_right₀, using that $\varphi>0$ so every inverse power is nonzero. No external lemmas beyond positivity of $\varphi$ are required.
why it matters
This is the ratio half of the module's main structural theorem echo_reflection_coefficient_forced, which packages the constant ratio together with the partition identity, the intensity relation $|R|^2 = \varphi^{-2}$, and the bounds $0 < |R| < 1$. It is also a field of the certificate echoReflectionCoefficientCert.
In the Recognition framework the claim closes the amplitude side of the GW-echo prediction: the scattering matrix of the barrier is fixed by $\varphi^2 = \varphi + 1$ alone (T6 self-similar fixed point), with no free parameter and no dimensional estimate. The geometric ratio $\varphi^{-1}$ is the same constant that appears as the Berry creation threshold and as the reciprocal of the golden rung spacing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.