barrier_total_reflection
plain-language theorem explainer
For a φ-self-similar near-horizon barrier with n rungs, the total echo amplitude after n reflections equals φ^{-n}. Anyone citing the RS black-hole echo prediction (geometric decay of successive echoes) uses this identity. The proof is definitional reflexivity: echo amplitude is defined as φ^{-1} raised to the rung count, matching the uniform per-rung reflection forced by self-similarity.
Claim. Let $B$ be a $\varphi$-self-similar barrier (rung scales $\ell_k=\ell_0\varphi^k$, with the same reflection amplitude $\varphi^{-1}$ at every rung). If $n$ is the number of rungs of $B$, then the echo amplitude after $n$ reflections equals $\varphi^{-n}$.
background
The module models the near-horizon recognition structure as a φ-self-similar potential barrier. Rung boundaries sit at scales $\ell_n=\ell_0\cdot\varphi^n$. At each boundary, energy splits by the golden-ratio partition $1=\varphi^{-1}+\varphi^{-2}$ (equivalent to $\varphi^2=\varphi+1$), so the single-rung reflection amplitude is $|R|=\varphi^{-1}$ and the intensity is $|R|^2=\varphi^{-2}$.
A PhiSelfSimilarBarrier packages a positive rung count together with the uniformity hypothesis that every rung has the same reflection amplitude $\varphi^{-1}$. The local echo-amplitude function is defined by $A_n:=(\varphi^{-1})^n$, matching the geometric product of $n$ identical reflections. Upstream, the same geometric form appears as $\varphi^{-n}$ in the BH-echo amplitude definition; the present module writes it as successive factors of $\varphi^{-1}$.
The round-trip phase per rung is $\log\varphi$, so echo $n$ arrives with amplitude $\varphi^{-n}$ and delay $n\cdot\Delta t_{\mathrm{echo}}$. The module status is structural: zero sorry, no RS-internal axiom.
proof idea
One-line definitional proof by rfl. The left-hand side is the local echo-amplitude function evaluated at the barrier's rung count; that function is defined as $(\varphi^{-1})^n$. The right-hand side is the same power. The barrier's uniformity field (reflection amplitude equals $\varphi^{-1}$ at every rung) is what makes the geometric product the correct total amplitude, but it is not needed as a rewrite step: equality holds by unfolding the definition alone.
why it matters
This is the amplitude half of the module's echo prediction: successive echoes decay geometrically by exactly $\varphi^{-1}$ per rung, with no free parameter. The module doc states the broader claim: the QG-paper echo prediction is not a dimensional-analysis estimate but a forced consequence of substrate self-similarity at golden-ratio spacing, via $\varphi^2=\varphi+1$ as the barrier scattering matrix.
Framework landmarks: φ is the T6 self-similar fixed point; the partition $1=\varphi^{-1}+\varphi^{-2}$ is the same golden identity that organizes the φ-ladder elsewhere in RS. The theorem closes the bookkeeping step from single-rung reflection to total $n$-rung amplitude inside Gravity.EchoReflectionCoefficient.
No downstream consumers are wired yet (used_by is empty). It sits ready for any theorem that quotes $A_n=\varphi^{-n}$ when assembling full echo trains (amplitude times delay $n\cdot(\log\varphi)/(2\pi f_{\mathrm{ringdown}})$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.