catalogAmplitude_pos
plain-language theorem explainer
The theorem shows that the catalog echo amplitude for any headline LIGO/Virgo event and echo index n is strictly positive. Gravitational-wave analysts would cite it when confirming non-zero signal strengths under phi-ladder damping. The proof is a one-line wrapper that reduces directly to the base positivity result for echoAmplitude.
Claim. For every canonical merger event $e$ and natural number $n$, the echo amplitude satisfies $0 < A(e,n)$, where $A(e,n)$ equals the base echo amplitude function independent of $e$.
background
The module models black-hole echo amplitudes via phi-ladder damping: each successive reflection off the bounce surface attenuates by one rung of recognition cost, so amplitudes follow $A_n = A_0 · φ^{-n}$. catalogAmplitude e n is defined identically to echoAmplitude n for each of the four headline events (GW150914, GW170817, GW190521, GW230529). The upstream theorem echoAmplitude_pos states 0 < echoAmplitude n and is proved by zpow_pos on Constants.phi_pos, using that φ > 1.
proof idea
The proof is a one-line wrapper that applies echoAmplitude_pos, since catalogAmplitude is definitionally equal to echoAmplitude.
why it matters
This supplies the positivity leg of the BH-echo amplitude certificate bhEchoAmplitudeCert. It underpins the module's structural claim that successive echo SNR ratios equal exactly 1/φ ≈ 0.618, a direct consequence of the phi-forced self-similar fixed point (T6) and the eight-tick octave structure. The module doc identifies the falsifier as any high-SNR merger whose echo ratios deviate systematically from 1/φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.