echo_geometric
plain-language theorem explainer
Echo amplitudes at successive φ-rungs form a geometric series with common ratio φ^{-1}. Black-hole echo and near-horizon barrier calculations in Recognition Science cite this identity to relate amplitudes across rung indices. The proof is a short term-mode algebraic reduction: unfold the amplitude definition, reassociate powers, and discharge the exponent arithmetic.
Claim. For natural numbers $n \le m$, the echo amplitude at rung $m$ equals $\varphi^{-(m-n)}$ times the echo amplitude at rung $n$: $A_m = \varphi^{-(m-n)} A_n$.
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}$ (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$ therefore arrives with amplitude decaying as a power of $\varphi^{-1}$ after $n$ rung reflections, and with round-trip phase $\log\varphi$ per crossing. The local scale ladder is the usual $\varphi^k$ spacing used elsewhere in the monolith (cf. cosmological scale defs). This theorem isolates the pure geometric relation among those amplitudes, independent of delay or phase bookkeeping.
proof idea
Term-mode proof. Unfold echoAmplitude (a pure power of $\varphi^{-1}$ in the rung index). Rewrite with ← pow_add so the exponents on the two sides match the claimed factor $\varphi^{-1}^{m-n}$. congr 1 reduces to equality of natural-number exponents; omega closes $m = (m-n) + n$ under the hypothesis $n \le m$. No external lemmas beyond power algebra and linear arithmetic.
why it matters
This is a structural identity in the Gravity echo-reflection development: the QG-paper echo train is forced by φ-self-similarity, not fitted. It makes precise the module claim that successive echoes form a geometric series with ratio $\varphi^{-1}$, which is exactly the single-rung reflection amplitude fixed by $\varphi^2 = \varphi + 1$ (T6: φ as the self-similar fixed point).
No downstream consumers are wired yet in the graph (used_by empty), so the result currently stands as a leaf lemma for amplitude bookkeeping beside siblings such as the reflected/transmitted fractions, reflectionAmplitude, and echoDampingFactor. It closes the algebraic half of the “no fitting parameter” claim for the barrier scattering matrix.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.