echoAmplitude_succ
plain-language theorem explainer
Successive gravitational-wave echo amplitudes form a geometric sequence with common ratio φ^{-1}. Anyone tracking black-hole echo trains from the golden-ratio barrier cites this recurrence to step the amplitude ladder. The proof unfolds the power definition, applies the successor law for powers, and closes by ring arithmetic.
Claim. For every natural number $n$, the amplitude of echo $n+1$ equals $\varphi^{-1}$ times the amplitude of echo $n$, where the $n$-th echo amplitude is defined by $(\varphi^{-1})^n$.
background
The module treats the near-horizon recognition structure as a φ-self-similar potential barrier. At each rung, energy splits by the golden-ratio partition $1=\varphi^{-1}+\varphi^{-2}$, equivalent to $\varphi^2=\varphi+1$. The single-rung reflected amplitude is therefore $|R|=\varphi^{-1}$, and echo $n$ arrives with amplitude scaling as $\varphi^{-n}$ after $n$ reflections.
In this file the amplitude is defined by $A(n)=(\varphi^{-1})^n$. Sibling modules write the same quantity as $\varphi^{-n}$ (or $(\varphi^n)^{-1}$); for $n\in\mathbb{N}$ these agree. The module also records the round-trip delay $n\cdot\Delta t_{\mathrm{echo}}$ with $\Delta t_{\mathrm{echo}}=(\log\varphi)/(2\pi f_{\mathrm{ringdown}})$, but that timing is not used here.
proof idea
Unfold $A(n)=(\varphi^{-1})^n$. On the left-hand side apply the power-successor identity $(\varphi^{-1})^{n+1}=(\varphi^{-1})\cdot(\varphi^{-1})^n$, then finish with ring arithmetic to match $\varphi^{-1}\cdot A(n)$. No external lemmas beyond pow_succ and ring; purely algebraic on the definition.
why it matters
The recurrence turns geometric decay of the echo train into an identity forced by the amplitude model, not a fitted damping. The module states that the QG-paper echo prediction is a forced consequence of substrate self-similarity at golden-ratio spacing: the reflection coefficient $|R|=\varphi^{-1}$ is fixed by $\varphi^2=\varphi+1$ alone, with no free parameter. This sits beside the partition identities (reflected/transmitted fractions summing to 1) and the damping-factor definitions in the same file. No recorded downstream dependents yet; it is structural bookkeeping for multi-echo amplitude chains in the gravity sector. Framework landmark: φ as the self-similar fixed point (T6) supplies the common ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.