echoAmplitude_strictly_decreasing
plain-language theorem explainer
The echo amplitude sequence defined by A_n = phi^{-n} satisfies A_{n+1} < A_n for every natural number n. Gravitational-wave analysts checking LIGO/Virgo black-hole merger echoes against the predicted phi-ladder damping would cite this result. The proof is a short algebraic reduction that rewrites the successor via the ratio lemma, invokes positivity and the bound phi > 1.5 to obtain phi^{-1} < 1, then closes with linear arithmetic.
Claim. For every natural number $n$, if $A_n = phi^{-n}$ denotes the echo amplitude at reflection number $n$ (relative to the primary), then $A_{n+1} < A_n$.
background
The module treats black-hole echo amplitudes under phi-ladder damping. The definition echoAmplitude n := phi^{-n} encodes attenuation by one recognition-cost rung per reflection off the bounce surface, so successive echoes are scaled by phi^{-1}. The module document states that the SNR ratio between the nth and (n-1)th echo is therefore exactly 1/phi ≈ 0.618 for every catalog event, compounding with the per-event delay certificate in BHEchoPerEventCatalog.
proof idea
The term proof first rewrites the goal with the successor-ratio lemma echoAmplitude_succ_ratio, reducing the claim to echoAmplitude n * phi^{-1} < echoAmplitude n. It obtains the positivity fact 0 < echoAmplitude n from echoAmplitude_pos. The inequality phi^{-1} < 1 is derived from phi > 1.5 (via Constants.phi_gt_onePointFive and inv_lt_one_of_one_lt₀). Linear arithmetic then finishes the comparison.
why it matters
The theorem supplies the strictly_decreasing field required by the downstream certificate bhEchoAmplitudeCert. It thereby completes the amplitude side of the black-hole echo prediction in the Gravity domain. Within Recognition Science the result instantiates the self-similar fixed point phi (T6) as the damping factor for gravitational-wave echoes, consistent with the eight-tick octave and D = 3 spatial structure; the module falsifier remains any high-SNR event whose successive echo ratios deviate systematically from 1/phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.