module module moderate

`IndisputableMonolith.Verification.GWTC3RingdownOneMemberDampingStatistic`

Records one-member QNM damping posterior summaries for the GWTC-3 ringdown event 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 samples below target. Downstream family-scaling modules cite these constants. The module is structural bookkeeping over the HDF5 sample summary, not a deep existence proof.

claimFor the single GWTC-3 ringdown member $S190727h$ (DS\_1mode\_10M), fix the RS damping target $\tau_{\mathrm{RS}}$ and the posterior damping sample statistics $\mu_\tau$, $\sigma_\tau$, median, and quantiles $q_{0.05},q_{0.16},q_{0.84},q_{0.95}$; define residual $\mu_\tau-\tau_{\mathrm{RS}}$, $z$-score $(\mu_\tau-\tau_{\mathrm{RS}})/\sigma_\tau$, fraction of samples below $\tau_{\mathrm{RS}}$, and mean $f_\tau$.

background

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

This module specializes that summary to the one-member damping statistic: named constants for the RS target, mean, standard deviation, median, outer and 1$\sigma$-style quantiles, residual and standardized residual from the mean, the fraction of posterior mass below the target, and the mean of $f_\tau$. Notation is ordinary sample statistics on the damping coordinate; no new physical law is introduced here.

The local setting is empirical closure bookkeeping inside the Verification domain: freeze the one-event numbers so controlled-family scalings can cite them without re-parsing HDF5.

proof idea

Definition and constant module over the upstream HDF5 sample summary. Sibling bindings name the RS damping target and the usual posterior summaries (mean, std, median, quantiles), then form residual and $z$ from the mean and the fraction of samples below target. No multi-step tactic proof is required beyond structural wiring of those values; the scientific content is the frozen statistic set, not a novel derivation.

why it matters in Recognition Science

Feeds IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily, which "records the first controlled-family scaling of the Session 123 one-member QNM damping statistic." Without a single-member freeze of mean, quantiles, residual, and fraction-below-target, family scaling has nothing stable to scale.

In the broader RS program this is empirical verification infrastructure rather than a forcing-chain step (T0–T8). It anchors ringdown damping comparisons for one GWTC-3 event so later modules can test whether the RS damping target sits consistently inside the posterior mass across a controlled family. Closure status on the upstream summary (0 sorry, 0 RS-internal axiom) is inherited as the data contract this module exposes.

scope and limits

Does not claim a full GWTC-3 catalog analysis; only one ringdown member (S190727h, DS_1mode_10M).
Does not derive the RS damping target from the forcing chain; it records and compares a fixed target.
Does not prove observational confirmation of RS; it freezes sample statistics for downstream tests.
Does not re-parse raw HDF5 strain; it depends on the upstream sample-summary module.
Does not address multi-mode or non-10M ringdown models beyond this named product.

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