echoAmplitude_pos
plain-language theorem explainer
The theorem asserts that the amplitude of the nth black-hole echo remains strictly positive for every natural number n. Gravitational-wave analysts would cite it when establishing lower bounds on signal strengths for echo searches in LIGO/Virgo data. The proof is a one-line wrapper that invokes zpow_pos on the positivity of the golden-ratio constant phi.
Claim. For every natural number $n$, the echo amplitude $A_n = phi^{-n}$ satisfies $A_n > 0$, where $phi$ is the golden ratio supplied by the Recognition Science constants bundle.
background
The module defines echo amplitudes under phi-ladder damping, where each successive reflection off the bounce surface attenuates the signal by one rung of recognition cost. The sibling definition echoAmplitude n returns phi raised to the power of negative n. This rests on the Constants structure from LawOfExistence, which packages the positive phi constant together with other CPM parameters, and matches the noncomputable echoAmplitude definition imported from GravitationalWaveEchoFromRS.
proof idea
The proof is a one-line wrapper that applies the lemma zpow_pos to Constants.phi_pos, with the exponent supplied by the negative of n cast to an integer.
why it matters
This supplies the positivity field for the BH-echo amplitude certificate bhEchoAmplitudeCert, which also bundles primary unity, one-step ratio, SNR ratio, and strict decrease. The module documentation states that the SNR of the nth echo relative to the previous is exactly 1/phi for every event; the result anchors that structural prediction inside the Recognition framework's phi-ladder damping, consistent with the self-similar fixed point forced at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.