gwtc3RingdownOneMemberDampingStatisticCert
plain-language theorem explainer
A certificate packages six numerical facts for one GWTC-3 ringdown sample: the RS damping target 1/φ sits inside the sample 68% and 90% damping intervals, the z-score from the mean is below one, the fraction below target is a proper probability, mean fτ exceeds the RS fτ target, and the HDF5 sample summary is inhabited. Verification and GW-echo workers cite it as the closed one-member damping check. The body is a pure structure instance wiring six already-proved norm_num lemmas.
Claim. The one-member GWTC-3 ringdown damping certificate holds: the RS target $1/\varphi$ lies strictly between the 5th and 95th percentiles and between the 16th and 84th percentiles of the derived per-cycle damping statistic; the absolute $z$-score of the target from the sample mean is less than $1$; the fraction of the sample 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. Frequency $f_{t_0}$ and damping time $\tau_{t_0}$ map to the per-cycle QNM damping ratio $\exp(-1/(f_{t_0}\tau_{t_0}))$. The RS structural echo damping target is $1/\varphi\approx 0.618$.
The certificate structure bundles: containment of that target in the central 90% and 68% intervals of the derived damping sample; a unit bound on the $z$-score from the mean; a fraction-below-target in $(0,1)$; mean $f\tau$ above the RS $f\tau$ floor; and availability of the upstream HDF5 sample-summary certificate. Sibling constants supply the concrete quantiles, mean, residual, and $z$-score for the range-read member rin_S190727h.
Each field is discharged upstream by unfolding those constants and applying norm_num. Module status is structural theorem: zero sorry, zero new RS-internal axioms.
proof idea
Pure structure instance. Each field is filled by a named theorem already closed by unfold plus norm_num on the concrete decimal constants: target inside the 90% interval, target inside the 68% interval, $z$-score from mean strictly below one, fraction below target in $(0,1)$, mean $f\tau$ above the RS floor, and nonempty sample-summary certificate. No extra reasoning occurs at this site.
why it matters
Directly feeds the inhabitedness theorem that asserts Nonempty of this certificate in one line. In the Recognition verification layer this is the first closed one-member comparison of a GWTC-3 ringdown QNM damping statistic against the RS echo-damping target $1/\varphi$ (the reciprocal of the golden ratio forced at T6 in the forcing chain). The module doc is explicit that the result is one-member only and does not identify single-mode QNM damping per cycle with the full RS echo-train damping observable; archive-wide lift and that identification remain open. Closure is recorded 2026-05-22 with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.