module module moderate

`IndisputableMonolith.Verification.GWTC3RingdownFamilyComparison`

Aggregates three controlled GWTC-3 ringdown damping families (DS one-mode at 10M, Kerr 220 at 0M, Kerr 220 at 10M) into a single comparison layer: total members/samples, mean and median gaps, and hit-count differences. Anyone building a family-stratified ringdown likelihood cites this module. The argument is structural bookkeeping over the three upstream family theorems, plus order lemmas on means, medians, and hits.

claimLet $\mathcal{F}_{\mathrm{DS}}$, $\mathcal{F}_{K,0}$, and $\mathcal{F}_{K,10}$ be the GWTC-3 ringdown damping families for DS one-mode at start window $10M$, Kerr $(2,2,0)$ at $0M$, and Kerr $(2,2,0)$ at $10M$. The module records family count, total members and samples, the mean gaps $\overline{d}_{\mathrm{DS}}-\overline{d}_{K,0}$ and $\overline{d}_{K,0}-\overline{d}_{K,10}$, the corresponding hit-count differences, and the order relations among family means, medians, and hit counts.

background

GWTC-3 ringdown analyses extract quasi-normal-mode (QNM) damping statistics from the post-merger waveform. Recognition Science verification packages these as controlled families: fixed mode content and fixed ringdown start-time window, so that scaling and selection statements stay comparable.

Three upstream modules supply the inputs. The DS one-mode $10M$ family is the first controlled-family scaling of the Session 123 one-member QNM damping statistic. The Kerr $220$ at $0M$ family is the first controlled Kerr-family scaling of that statistic. The Kerr $220$ at $10M$ family keeps the same Kerr $220$ mode but moves the start window to $10M$.

This module does not re-derive those family statistics. It only assembles them into one comparison surface: counts, mean/median gaps, hit differences, and order lemmas that a downstream selector can quote without reopening the family proofs.

proof idea

Definitional layer first: constants for family count, total members, and total samples, plus named differences of family means and of hit counts (DS versus Kerr $0M$, Kerr $0M$ versus Kerr $10M$).

Theorems then discharge the bookkeeping identities for totals and the order statements on means, medians, and hit counts. Each order lemma is a short comparison over the three already-proved family aggregates; there is no new waveform or QNM analysis inside this file. Structure is import-three-families, name the gaps, prove the orders.

why it matters in Recognition Science

The immediate parent is the GWTC-3 ringdown family-stratified likelihood selector, which imports this module as the comparison surface for eligible families. That selector records the policy for future GWTC-3 ringdown likelihoods; without a single place that orders DS versus Kerr windows and hit rates, the selector would have to inline three family modules.

In the broader verification stack this is structural closure (zero sorry, no RS-internal axiom on the upstream family theorems), not a new forcing-chain step. It does not touch T5–T8, the Recognition Composition Law, or the mass ladder. Its job is narrower: make controlled-family damping comparisons citeable so likelihood stratification stays deterministic and auditable.

scope and limits

Does not re-derive QNM frequencies or damping times from raw GWTC-3 strain.
Does not claim a physical preference for DS over Kerr; only records ordered family aggregates.
Does not fix ringdown start time or mode content beyond the three imported families.
Does not construct the likelihood functional; that lives in the selector module.
Does not address non-GWTC-3 catalogs or multi-mode families outside the named set.

used by (1)

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

IndisputableMonolith.Verification.GWTC3RingdownLikelihoodSelector module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily module_import
IndisputableMonolith.Verification.GWTC3RingdownKerr2200MDampingFamily module_import
IndisputableMonolith.Verification.GWTC3RingdownKerr22010MDampingFamily module_import

declarations in this module (18)

def comparisonFamilyCount L41
def comparisonTotalMembers L42
def comparisonTotalSamples L43
def dsMeanMinusKerr0Mean L44
def kerr0MeanMinusKerr10Mean L45
def dsHitDiffVsKerr0 L46
def kerr0HitDiffVsKerr10 L47
theorem comparison_total_members L51
theorem comparison_total_samples L57
theorem family_mean_order L64
theorem family_median_order L69
theorem hit_count_order L75
theorem ds_mean_difference_pos L81
theorem kerr_mean_difference_pos L86
structure GWTC3RingdownFamilyComparisonCert L93
def gwtc3RingdownFamilyComparisonCert L113
theorem gwtc3RingdownFamilyComparisonCert_inhabited L124
theorem gwtc3_ringdown_family_comparison_one_statement L129