GWTC3RingdownOneMemberDampingStatisticCert
plain-language theorem explainer
Certificate packing the one-member GWTC-3 ringdown damping comparison: the RS echo-damping target $1/\varphi$ sits inside the sample's central 68% and 90% posterior intervals, the mean-standardized residual is below 1, the below-target fraction is in $(0,1)$, mean $f\tau$ exceeds the RS $f\tau$ target, and an HDF5 sample-summary cert is nonempty. Downstream one-statement and DS1-mode family certificates inhabit or extend it. Pure structure definition; no proof body.
Claim. A certificate asserting six facts for the mapped one-member GWTC-3 ringdown damping-per-cycle posterior: the RS damping target $1/\varphi$ lies strictly between the 5th and 95th percentiles and between the 16th and 84th percentiles; the $z$-score of the target relative to the sample mean is less than $1$; the fraction of posterior mass below the target lies in $(0,1)$; the mean $f\tau$ exceeds the RS $f\tau$ target; and a nonempty HDF5 sample-summary certificate is available.
background
This module records the first physically mapped one-member GWTC-3 ringdown statistic. Posterior samples of frequency $f_{t_0}$ and damping time $\tau_{t_0}$ are converted to a per-cycle QNM damping ratio
$$\mathrm{damping_per_cycle}=\exp\bigl(-1/(f_{t_0}\tau_{t_0})\bigr).$$
The Recognition Science structural echo-damping target is $1/\varphi\approx 0.618$. For the range-read member rin_S190727h_pyring_DS_1mode_10M.h5, empirical quantiles of that derived damping (5th $\approx 0.279$, 16th $\approx 0.553$, 84th $\approx 0.950$, 95th $\approx 0.970$) and the below-target fraction ($\approx 0.208$) are frozen as constants.
Upstream, GWTC3RingdownHDF5SampleSummaryCert certifies that the member name, posterior path, sample count, and field count match the schema and that the sample count is positive. The present structure only packages the numerical comparison predicates against those frozen statistics; it does not re-derive the HDF5 read.
proof idea
No proof body: this is a structure definition whose fields are propositions. Each field is a named inequality or a Nonempty witness over already-defined real constants (dampingQ05, dampingQ16, dampingQ84, dampingQ95, dampingZFromMean, dampingFractionBelowTarget, ftauMean) and the RS targets. Inhabitation is discharged downstream by a concrete term that plugs in the corresponding proved inequalities (damping_target_inside_90_interval, damping_target_inside_68_interval, damping_z_from_mean_lt_one, etc.).
why it matters
Closes the one-member damping comparison leg of the GWTC-3 ringdown verification stack (module status: structural theorem, 0 sorry, 0 new RS axioms, closure 2026-05-22). The target $1/\varphi$ is the Berry creation threshold from the RS primer; placing it inside the observed 68% and 90% bands is the first concrete LIGO/Virgo posterior check of that constant on a mapped QNM damping observable.
Downstream, gwtc3RingdownOneMemberDampingStatisticCert inhabits the structure, gwtc3RingdownOneMemberDampingStatisticCert_inhabited and gwtc3_ringdown_one_member_damping_statistic_one_statement export a single conjunction, and GWTC3RingdownDS1Mode10MDampingFamilyCert lifts the comparison toward the damped-sinusoid family (pooled 90% band, taxonomy counts). The module itself flags the open gap: this is not archive-wide and does not identify single-mode QNM damping-per-cycle with the final RS echo-train damping observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.