fraction_above_target_small
plain-language theorem explainer
The GWTC-3 ringdown posterior sample fraction with log-amplitude above the RS target log(φ^{-44}) is strictly less than 0.1%. Anyone citing the one-member S190727h amplitude-scale check uses this bound. The proof unfolds the recorded fraction 0.000331 and closes by numerical normalization.
Claim. The recorded sample fraction of posterior draws with $\log A_{t_0}$ above the RS structural target $\log(\varphi^{-44})$ satisfies $f_{\mathrm{above}} < 0.001$.
background
This module freezes a one-member RS amplitude-scale comparison on the GWTC-3 ringdown HDF5 table for event S190727h (rin_S190727h_pyring_DS_1mode_10M.h5), column logA_t_0 of /EXP6/posterior_samples. The RS structural target is $\log(\varphi^{-44}) \approx -21.173$, while the posterior mean sits near $-22.245$ with std $\approx 0.398$.
Among the recorded summary numbers is the sample fraction of draws above that target, fixed as the real constant $0.000331$. Sibling quantities include residual and $z$-score from the mean, quantile cutoffs (5/16/84/95%), and the explicit target value. The module is a structural verification record only: it does not identify $\log A_{t_0}$ as the final RS echo observable, nor does it form an archive-wide likelihood.
proof idea
One-line numerical check. Unfold the definition of the recorded fraction (the constant $0.000331$), then apply norm_num to discharge $0.000331 < 0.001$ in $\mathbb{R}$. No lemmas beyond definitional unfolding are required.
why it matters
Feeds the bundled one-statement theorem gwtc3_ringdown_one_member_rs_statistic_one_statement, which conjoins the 95% quantile bound, $z>2$ from the mean, this fraction bound, and nonemptiness of the certificate record. Also appears among the fields assembled into gwtc3RingdownOneMemberRSStatisticCert.
In the Recognition framework this is a verification-layer fact, not a forcing-chain step: it documents that on this single GWTC-3 ringdown member the RS rung target $\log(\varphi^{-44})$ lies in a thin upper tail (fraction $\sim 3.3\times 10^{-4}$). It supports the structural claim that the target is outside the bulk posterior mass, complementary to the $z\approx 2.69$ and quantile inequalities. It does not close any open identification of the echo amplitude observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.