module module moderate

`IndisputableMonolith.Verification.GWTC3RingdownOneMemberDampingStatistic`

Records the one-member QNM damping posterior summary for the GWTC-3 ringdown sample S190727h (DS_1mode_10M). Defines the RS damping target, sample mean/std/median/quantiles, residual and z-score from the mean, and the fraction of draws below target. Downstream family-scaling modules cite these constants. The content is structural bookkeeping of extracted HDF5 posterior numbers, not a deep derivation.

claimFor the single GWTC-3 ringdown member $S190727h$ (DS\_1mode\_10M), fix the RS damping target $\tau_{\mathrm{RS}}$ and the posterior summary statistics of the damping time: mean $\mu$, standard deviation $\sigma$, median, quantiles $q_{0.05}, q_{0.16}, q_{0.84}, q_{0.95}$, residual $\mu - \tau_{\mathrm{RS}}$, $z$-score $(\mu - \tau_{\mathrm{RS}})/\sigma$, fraction of posterior mass below $\tau_{\mathrm{RS}}$, and mean $f_\tau$.

background

Recognition Science verification against LIGO/Virgo GWTC-3 ringdown data proceeds by reading published HDF5 posterior samples for quasi-normal-mode (QNM) damping times and comparing them to an RS-native target. The upstream module GWTC3RingdownHDF5SampleSummary is a structural theorem (0 sorry) that records the first posterior-summary statistics extracted from a range-read GWTC-3 ringdown HDF5 file for member rin/rin_S190727h_pyring_DS_1mode_10M.h5.

This module specializes that sample to the one-member damping statistic. Sibling definitions name the RS damping target, the usual location/scale summaries (mean, std, median, outer and 1$\sigma$ quantiles), the residual and standardized residual of the mean from the target, the posterior fraction lying below the target, and the mean of the dimensionless damping factor $f_\tau$.

The local setting is pure verification bookkeeping: numerical constants frozen from the HDF5 draw, exposed as Lean definitions so later family and multi-event modules can cite them without re-parsing files.

proof idea

Definition and constant module, not a multi-step proof development. Values are pinned by the upstream HDF5 sample summary for S190727h DS_1mode_10M; this file packages the one-member damping view (target, moments, quantiles, residual, $z$, fraction below target, $f_\tau$ mean) as named Lean objects. Any one-statement theorem in the module is a thin wrapper asserting those recorded equalities, with no independent analytic argument.

why it matters in Recognition Science

Feeds the controlled-family scaling layer. Downstream GWTC3RingdownDS1Mode10MDampingFamily imports this module and records "the first controlled-family scaling of the Session 123 one-member QNM damping statistic." Without a frozen one-member baseline (target, mean residual, $z$, fraction below target), family comparisons across modes or events have no anchor.

In the broader RS verification domain this is empirical contact, not a forcing-chain step (T0–T8). It ties the abstract damping prediction to a concrete GWTC-3 ringdown posterior so later modules can state how far the data sit from the RS target and whether family structure tightens or loosens that tension.

scope and limits

Does not claim a full GWTC-3 catalog analysis; only the single member S190727h DS_1mode_10M.
Does not derive the RS damping target from first principles; it consumes a fixed target value.
Does not re-read or validate the HDF5 file; numbers are inherited from the upstream sample summary.
Does not address frequency (real-part) QNM statistics, only damping.
Does not assert observational confirmation or falsification of Recognition Science.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSummary module_import

declarations in this module (23)

def rsDampingTarget L37
def dampingMean L38
def dampingStd L39
def dampingMedian L40
def dampingQ05 L41
def dampingQ16 L42
def dampingQ84 L43
def dampingQ95 L44
def dampingResidualFromMean L45
def dampingZFromMean L46
def dampingFractionBelowTarget L47
def ftauMean L48
def rsFtauTarget L49
theorem damping_target_inside_90_interval L53
theorem damping_target_inside_68_interval L58
theorem damping_z_from_mean_lt_one L63
theorem damping_fraction_below_target_between_zero_and_one L68
theorem ftau_mean_gt_rs_target L73
theorem sample_summary_available L78
structure GWTC3RingdownOneMemberDampingStatisticCert L84
def gwtc3RingdownOneMemberDampingStatisticCert L95
theorem gwtc3RingdownOneMemberDampingStatisticCert_inhabited L104
theorem gwtc3_ringdown_one_member_damping_statistic_one_statement L109