echoAmplitude_zero
plain-language theorem explainer
The zeroth gravitational-wave echo has unit relative amplitude: the primary signal before any barrier reflection. Anyone normalizing the φ-ladder echo train against the ringdown cites this base case. The proof is a one-line unfold of the geometric amplitude definition, then simplification of the zero power.
Claim. The echo amplitude at reflection count $0$ equals $1$: $(\varphi^{-1})^{0} = 1$ (equivalently $\varphi^{0} = 1$).
background
This 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 exactly $\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 assigned amplitude proportional to $\varphi^{-n}$ (geometric decay from $n$ successive reflections) and delay $n \cdot \Delta t_{\mathrm{echo}}$. The local definition writes this as $(\varphi^{-1})^{n}$; sibling modules use the equivalent forms $\varphi^{-n}$ and $(\varphi^{n})^{-1}$.
The present statement is the $n = 0$ normalization of that geometric sequence: no reflection yet, amplitude one relative to the primary.
proof idea
One-line wrapper. Unfold the local definition of echo amplitude (which is $(\varphi^{-1})^{n}$), then simp reduces the zero exponent to $1$. No external lemmas are required beyond the definition and ordinary power arithmetic in $\mathbb{R}$.
why it matters
It fixes the base of the echo train so later amplitudes $\varphi^{-n}$ are dimensionless ratios to the primary ringdown, not free scales. The module's claim is that the QG-paper echo prediction is forced by the substrate's self-similar structure at golden-ratio spacing, not a dimensional fit; the reflection coefficient $|R| = \varphi^{-1}$ is read off $\varphi^{2} = \varphi + 1$ alone (primer landmark T6: $\varphi$ as the self-similar fixed point).
No downstream theorems currently depend on this declaration. It still anchors the structural story: without unit primary amplitude, the geometric decay and the partition identities (reflected/transmitted fractions summing to one) would float. Sibling results on positivity, strict sub-unity reflection, and the damping factor sit on the same definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.