echoAmplitude_one
plain-language theorem explainer
The theorem establishes that the echo amplitude at reflection number zero equals unity under phi-ladder damping. Gravitational-wave analysts would cite it to anchor the base of the amplitude sequence when testing predicted echo strengths against LIGO/Virgo data. The proof is a one-line simplification that unfolds the definition of echoAmplitude.
Claim. Let $A_n = phi^{-n}$ denote the echo amplitude at reflection number $n$. Then $A_0 = 1$.
background
The Black-Hole Echo Amplitudes module models successive reflections off the bounce surface with phi-ladder damping, so that each echo is attenuated by one rung of recognition cost. The definition echoAmplitude n := phi ^ (-n) encodes this directly, with n = 0 for the primary signal. This setting compounds with the per-event catalog from BHEchoPerEventCatalog and draws on the equivalent definition supplied by GravitationalWaveEchoFromRS.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of echoAmplitude, which reduces phi^0 directly to 1.
why it matters
The result supplies the primary_unity field inside bhEchoAmplitudeCert, which assembles the full amplitude certificate including positivity, one-step ratio, SNR ratio, and strict decrease. It supplies the base case for the phi-ladder prediction in the gravity module, consistent with the phi fixed point and eight-tick octave from the forcing chain. The module states the falsifier explicitly: any high-SNR merger whose successive echo-amplitude ratios deviate systematically from 1/phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.