echoAmplitudeDecay
plain-language theorem explainer
Echo amplitudes in the RS gravitational wave model decay by the exact factor phi inverse between successive reflections. Analysts constructing black hole bounce echo trains cite this ratio when fixing the amplitude component of the five-parameter set. The term proof unfolds the negative-power definition, invokes positivity to obtain a non-zero fact, and cancels via field simplification.
Claim. For any natural number $k$, if the echo amplitude after $n$ reflections is defined by $A(n) = phi^{-n}$, then $A(k+1)/A(k) = phi^{-1}$.
background
The module treats gravitational wave echoes from black hole bounces in Recognition Science. Echo amplitude at reflection count $n$ is defined as $phi^{-n}$, implementing geometric suppression by $1/phi$ per echo. This sits with the delay formula $2 r_min log phi$, where $r_min$ is the nuclear saturation radius, and the five parameters match config dimension $D=5$ as stated in the module documentation.
proof idea
The term proof unfolds echoAmplitude to expose the ratio of powers. It obtains a non-zero hypothesis from pow_pos applied to phi_pos, rewrites the successor exponent, and finishes by field_simp using the non-zero lemmas for phi.
why it matters
The result supplies the amplitude_decay field inside gwEchoCert, the certificate assembling all five echo parameters. It realizes the per-rung decay phi^{-k} asserted in the module documentation. The step embeds the phi-ladder suppression into the gravitational wave echo model, consistent with the self-similar fixed point structure of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.