echoAmplitude
plain-language theorem explainer
echoAmplitude defines the amplitude of the k-th gravitational wave echo as the reciprocal of phi to the power k. Researchers modeling black hole echo sequences in the Recognition Science framework cite it for the geometric decay law per reflection. It is supplied as a direct noncomputable definition that assigns the value without invoking lemmas or further reduction.
Claim. The amplitude of the gravitational wave echo at reflection number $k$ equals $phi^{-k}$, where $phi$ is the golden ratio.
background
The GravitationalWaveEchoFromRS module treats gravitational wave echoes in strong-field regimes by adding amplitude decay to the existing delay formula. Module documentation states that each successive echo is suppressed by the factor $1/phi$, yielding five canonical parameters (delay, amplitude, frequency, phase, quality) that match configuration dimension D=5. This definition mirrors the upstream echoAmplitude from BHEchoAmplitudes, which sets the value to $phi^{-n}$ for reflection count n.
proof idea
The declaration is a direct definition that sets echoAmplitude k to the multiplicative inverse of phi raised to k. No lemmas are applied and no tactics are used; it functions as a one-line abbreviation relying on the phi constant imported from Constants.
why it matters
This definition supplies the amplitude component required by BHEchoAmplitudeCert, which certifies positivity for all n, unity at n=0, the one-step ratio phi inverse, and strict decrease. It completes the echo decay law in the RS strong-field model, consistent with the phi-ladder and the five-parameter echo structure. It supports downstream cataloging of amplitudes for headline events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.