GWTC3RingdownFamilyComparisonCert
plain-language theorem explainer
Certificate type for the three-family GWTC-3 ringdown comparison: member and sample counts of DS_1mode_10M, Kerr_220_0M, and Kerr_220_10M sum to the comparison totals, and pooled means, medians, and 68%-hit counts strictly order as Kerr_220_10M < Kerr_220_0M < DS_1mode_10M, with each family cert inhabited. Downstream one-statement comparison theorems and the likelihood selector inhabit or consume it. Pure structure definition; no proof body.
Claim. A certificate asserting: (i) the three mapped damping families (damped-sinusoid 1-mode at $10M$, Kerr $220$ at $0M$, Kerr $220$ at $10M$) have member counts and total sample counts that sum to the comparison aggregates; (ii) pooled means, pooled medians, and counts of members inside the pooled 68% interval strictly increase in the order Kerr$_{220,10M}$ $<$ Kerr$_{220,0M}$ $<$ DS$_{1\mathrm{mode},10M}$; (iii) each of the three family certificates is inhabited.
background
The module aggregates three currently mapped GWTC-3 ringdown damping families: DS_1mode_10M, Kerr_220_0M, and Kerr_220_10M. Status is structural (zero sorry, zero new RS-internal axioms). It records model and start-time dependence: mean and median order DS > Kerr_0M > Kerr_10M, and target inclusion degrades along the same order (DS: target in pooled 68% and 90%; Kerr_0M: 90% only; Kerr_10M: neither).
Upstream family modules supply concrete Nat and real constants used as field sides: e.g. DS member count 22, total samples 643624, members inside 68% equal to 13, pooled mean $\approx 0.58126$, pooled median $\approx 0.56966$, plus the DS family certificate structure (member-count taxonomy match, positivity, target-inside-pooled-90, etc.). Parallel Kerr family modules supply the analogous Kerr counts and pooled statistics.
This is a three-family controlled comparison only, not a mixed-model archive-wide likelihood. Comparison totals and ordering lemmas live as siblings in the same module.
proof idea
No proof body: the declaration is a structure (certificate type). Each field is a Prop constraining named constants from the three family modules and local comparison aggregates. Inhabitation is discharged downstream by gwtc3RingdownFamilyComparisonCert, which fills the fields with sibling lemmas comparison_total_members, comparison_total_samples, family_mean_order, family_median_order, hit_count_order, and the three family-cert Nonempty witnesses.
why it matters
Packages the controlled-family comparison that the module advertises as closed. Immediate consumers: the concrete inhabitant gwtc3RingdownFamilyComparisonCert, the Nonempty theorem, and the one-statement theorem bundling family count 3, total members 66, total samples 1954998, and the mean/median/hit orderings. Also feeds GWTC3RingdownLikelihoodSelectorCert, which ties selector-eligible files and models to this comparison partition.
In the Recognition verification layer this is empirical closure infrastructure for ringdown damping-model dependence, not a forcing-chain (T0–T8) step. It locks the three-family ordering and availability facts so later selector and archive claims can cite a single inhabited certificate rather than re-proving the inequalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.