module module moderate

`IndisputableMonolith.Verification.GWTC3RingdownKerr2200MDampingFamily`

Records the controlled Kerr 220 quasi-normal-mode damping family for GWTC-3 ringdown at the 0M start-time window: member, event, and sample counts plus pooled mean, std, median, and quantile summaries against the RS damping target. Downstream comparison and guarded-script modules import these constants. Structural bookkeeping closed with zero sorry; the argument is archive taxonomy plus pooled posterior aggregates, not a dynamical derivation.

claimFor the Kerr$_{220}$ ringdown family at start time $0M$, the module fixes the model label, member/event/total-sample counts, the RS damping target, and the pooled damping statistics (mean, standard deviation, median, $Q_{05}$, $Q_{16}$, $Q_{84}$, $Q_{95}$) over the family's posterior samples.

background

GWTC-3 ringdown verification in this tree is built on an archive-wide filename taxonomy of the 243 HDF5 files in IGWN-GWTC3-TGR-v1-rin.zip, read only from the ZIP central directory (no posterior samples at taxonomy time). That taxonomy classifies controlled analysis families by QNM mode content and ringdown start-time window.

The first controlled-family damping statistic was the $DS_{1\mathrm{mode},10M}$ family. The present module is the matching Kerr-family record at the $0M$ window: same Kerr 220 mode bookkeeping pattern, different start-time cut. Sibling constants name the model, counts, RS damping target, and pooled location/scale quantiles of the damping statistic.

Status across the chain is structural theorem: zero sorry, zero RS-internal axiom, closure dated 2026-05-22. The local claim is one-statement Kerr-family damping bookkeeping, not a new forcing-chain step.

proof idea

Definition-and-constant module, not a multi-step proof script. It imports the filename taxonomy and the prior $DS_{1\mathrm{mode},10M}$ family pattern, then records named constants for the Kerr$_{220}$/$0M$ family: model name, member/event/sample counts, RS damping target, and pooled mean, std, median, and five quantile levels. Any theorem wrappers are one-line structural assertions that these recorded values inhabit the expected types and comparison interfaces. No dynamical QNM derivation is performed here.

why it matters in Recognition Science

This module is the Kerr${220}$/$0M$ leaf in the controlled-family damping ladder. GWTC3RingdownFamilyComparison aggregates the three currently mapped damping families, explicitly listing $DS{1\mathrm{mode},10M}$ and $\mathrm{Kerr}_{220,0M}$; without these constants the comparison has nothing to stack. GWTC3RingdownGuardedFamilyScripts wires the runtime family guard into the mapped family-statistic scripts, so the Kerr $0M$ labels must be present as a guarded target. The sibling GWTC3RingdownKerr22010MDampingFamily keeps the same Kerr 220 mode and only changes the start-time window to $10M$, making this module the $0M$ baseline of that pair. In the broader RS verification story it is empirical closure against GWTC-3 ringdown posteriors, not a T0–T8 forcing step.

scope and limits

Does not derive QNM frequencies or damping rates from the RS forcing chain.
Does not read or re-analyze raw GW strain; only records family-level pooled summaries.
Does not claim the 10M Kerr window; that is a separate sibling module.
Does not assert a full GR vs RS hypothesis test beyond recorded pooled statistics.
Does not extend the filename taxonomy; it consumes the existing archive classification.

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.GWTC3RingdownKerr22010MDampingFamily module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily module_import
IndisputableMonolith.Verification.GWTC3RingdownFilenameTaxonomy module_import

declarations in this module (28)

def kerr2200ModelName L59
def kerr2200MemberCount L60
def kerr2200EventCount L61
def kerr2200TotalSampleCount L62
def kerr2200RSDampingTarget L63
def kerr2200PooledMean L64
def kerr2200PooledStd L65
def kerr2200PooledMedian L66
def kerr2200PooledQ05 L67
def kerr2200PooledQ16 L68
def kerr2200PooledQ84 L69
def kerr2200PooledQ95 L70
def kerr2200PooledZFromMean L71
def kerr2200PooledFractionBelowTarget L72
def kerr2200MembersInside68Count L73
theorem kerr2200_member_count_pos L77
theorem kerr2200_event_count_pos L81
theorem kerr2200_sample_count_pos L85
theorem kerr2200_target_inside_pooled_90 L89
theorem kerr2200_target_not_inside_pooled_68 L95
theorem kerr2200_z_from_mean_gt_one L100
theorem kerr2200_fraction_below_target_valid L105
theorem kerr2200_members_inside68_nonzero L110
theorem ds_vs_kerr_mean_order L115
structure GWTC3RingdownKerr2200MDampingFamilyCert L122
def gwtc3RingdownKerr2200MDampingFamilyCert L141
theorem gwtc3RingdownKerr2200MDampingFamilyCert_inhabited L155
theorem gwtc3_ringdown_kerr2200m_damping_family_one_statement L160