echo_sensitivity_pos
plain-language theorem explainer
The black-hole echo phenomenology dataset attachment carries a strictly positive numerical sensitivity (0.10 in amplitude-ratio units). Anyone assembling the quantum-gravity falsifier register or the GWTC-3 echo status certificate cites this positivity fact. The proof is a direct numerical check after unfolding the attachment record and the positivity predicate.
Claim. The LIGO/Virgo/KAGRA GWTC-3 post-merger echo-search attachment has positive sensitivity: if $S$ denotes its reported sensitivity in echo amplitude-ratio units, then $0 < S$ (concretely $S = 0.10$).
background
This module attaches named observational channels and numerical scales to every row of the quantum-gravity master-plan falsifier register. Each DatasetAttachment records a sector, dataset name, units, a sensitivity figure, an RS target scale, and an honesty flag about whether current data already reach that target. The purpose is falsifiability accounting, not empirical confirmation of RS.
Positive sensitivity is the predicate $0 < D.\mathrm{sensitivity}$. The echo row is the black-hole echo phenomenology attachment: GWTC-3 tests of GR report no post-merger echoes in the analyzed events, with sensitivity $0.10$ in echo amplitude-ratio units. The RS echo-damping target on that row is the dimensionless amplitude ratio $1/\varphi \approx 0.618$.
proof idea
Term-mode proof by unfolding. Expand the positivity predicate to $0 < D.\mathrm{sensitivity}$ and the echo attachment to its concrete field values, then discharge $0 < 0.10$ by norm_num. No lemmas beyond definitional unfolding are required.
why it matters
This is one of the per-row positivity witnesses that close the structural certificate for the falsifier-register dataset attachments (zero sorry, zero new RS axioms). It is packed into the register certificate record and into the one-statement conjunction asserting that every falsifier-register row has positive sensitivity and positive RS target scale.
Downstream, the GWTC-3 ringdown status module pairs it with the matching target-scale positivity fact to certify that the echo row is numerically well-formed. In the RS framework the echo target $1/\varphi$ is the Berry-scale amplitude ratio tied to the golden ratio forced at T6; the sensitivity witness only guarantees the comparison is non-vacuous, not that GWTC-3 has already ruled the prediction in or out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.