module module high

`IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily`

Records the controlled DS_1mode_10M ringdown damping family from GWTC-3: pooled mean, std, median, and quantile statistics of the per-cycle QNM damping ratio, plus member/event/sample counts and the RS damping target. Downstream family-comparison and guarded-script modules import these constants. The module is a structural data theorem: named numeric aggregates over the taxonomy-filtered archive, with no sorry.

claimFor the controlled GWTC-3 ringdown family $\mathrm{DS\_1mode\_10M}$, the module fixes the model name, member/event/total-sample counts, the Recognition Science damping target, and the pooled posterior statistics $\mu$, $\sigma$, median, and quantiles $Q_{05}, Q_{16}, Q_{84}, Q_{95}$ of the per-cycle QNM damping ratio built from $f_{t_0}$ and $\tau_{t_0}$.

background

GWTC-3 ringdown verification in this tree is built from a filename taxonomy of the 243 HDF5 files in IGWN-GWTC3-TGR-v1-rin.zip (ZIP central directory only; no posterior samples read at taxonomy time). That taxonomy is a closed structural theorem.

The one-member damping statistic maps ringdown frequency and damping time $(f_{t_0}, \tau_{t_0})$ to a per-cycle QNM damping ratio. This module lifts that one-member map to a named controlled family $\mathrm{DS_1mode_10M}$: fixed model label, counts of members/events/samples, an RS-native damping target, and pooled location/scale/quantile summaries of the damping ratio across the family.

Sibling constants expose those aggregates (dsPooledMean, dsPooledStd, median and $Q_{05}$–$Q_{95}$, counts, and dsRSDampingTarget) for import by comparison and scripting layers.

proof idea

Definition-and-constant module, not a multi-step tactic proof. It packages the DS_1mode_10M family as named Lean values: model name string, integer member/event/sample counts, the RS damping target, and pooled mean/std/median/quantile floats derived from the one-member damping statistic under the filename taxonomy filter. Argument structure is archival closure: import taxonomy + one-member statistic, emit the family aggregate table as zero-sorry structural data for downstream modules.

why it matters in Recognition Science

Supplies the first of the three currently mapped damping families aggregated in the controlled-family comparison module (DS_1mode_10M alongside Kerr_220_0M). Family-comparison and guarded family-script modules import it so Session-133 runtime guards and cross-family tables can cite a single closed DS family object rather than ad hoc numbers.

The Kerr_220_0M family module is a parallel controlled scaling; together they form the comparison spine. In the broader Recognition verification stack this is empirical ringdown bookkeeping against an RS damping target, not a derivation of $J$, $\varphi$, or the forcing chain (T5–T8). It closes a structural data step so later claims can quote pooled DS damping without reopening the archive layout.

scope and limits

Does not claim a full GWTC-3 catalog reanalysis or new posterior sampling.
Does not prove Kerr QNM uniqueness or derive the RS damping target from T5–T8.
Does not read HDF5 posterior samples inside this module body; it records family aggregates.
Does not compare families; comparison lives in the downstream family-comparison module.
Does not assert observational discovery beyond the archived structural constants.

used by (3)

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

IndisputableMonolith.Verification.GWTC3RingdownFamilyComparison module_import
IndisputableMonolith.Verification.GWTC3RingdownGuardedFamilyScripts module_import
IndisputableMonolith.Verification.GWTC3RingdownKerr2200MDampingFamily module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownFilenameTaxonomy module_import
IndisputableMonolith.Verification.GWTC3RingdownOneMemberDampingStatistic module_import

declarations in this module (27)

def dsFamilyModelName L53
def dsFamilyMemberCount L54
def dsFamilyEventCount L55
def dsFamilyTotalSampleCount L56
def dsRSDampingTarget L57
def dsPooledMean L58
def dsPooledStd L59
def dsPooledMedian L60
def dsPooledQ05 L61
def dsPooledQ16 L62
def dsPooledQ84 L63
def dsPooledQ95 L64
def dsPooledZFromMean L65
def dsPooledFractionBelowTarget L66
def dsMembersInside68Count L67
theorem ds_family_member_count_matches_taxonomy L71
theorem ds_family_event_count_pos L74
theorem ds_family_sample_count_pos L78
theorem ds_target_inside_pooled_90 L82
theorem ds_target_inside_pooled_68 L87
theorem ds_z_from_mean_lt_one L92
theorem ds_fraction_below_target_valid L97
theorem ds_members_inside68_nonzero L102
structure GWTC3RingdownDS1Mode10MDampingFamilyCert L109
def gwtc3RingdownDS1Mode10MDampingFamilyCert L126
theorem gwtc3RingdownDS1Mode10MDampingFamilyCert_inhabited L139
theorem gwtc3_ringdown_ds1mode10m_damping_family_one_statement L144