comparisonFamilyCount
plain-language theorem explainer
Fixes the number of controlled GWTC-3 ringdown damping families in this comparison at three. Downstream one-statement theorems cite it to lock the family count before ordering means, medians, and target-inclusion rates. The body is a literal natural-number definition.
Claim. The controlled GWTC-3 ringdown comparison comprises exactly three damping families.
background
The module aggregates three currently mapped GWTC-3 ringdown damping families: the single-mode dynamical-spacetime family started at $10M$ (DS_1mode_10M), and the Kerr $(2,2,0)$ families started at $0M$ and $10M$ (Kerr_220_0M, Kerr_220_10M). It is a structural verification layer: zero sorry, no new RS-internal axioms, and explicitly not an archive-wide mixed-model likelihood.
The comparison proves model and start-time dependence: mean and median damping statistics decrease in the order DS then Kerr-$0M$ then Kerr-$10M$, and target inclusion in pooled 68% and 90% intervals degrades along the same order. This constant simply records that the controlled set has cardinality three.
proof idea
Definitional abbreviation: the natural number is set equal to $3$ with no proof obligations, lemmas, or tactics.
why it matters
Pins the family cardinality that the parent theorem gwtc3_ringdown_family_comparison_one_statement conjoins with total member count, total sample count, and the strict mean order
$\mathrm{Kerr}{220,10M}<\mathrm{Kerr}{220,0M}<\mathrm{DS}$. Without a fixed count, the three-family mean/median/hit-count orderings would be ill-scoped. In the Recognition verification stack this is bookkeeping for a controlled GWTC-3 ringdown check, not a forcing-chain (T0–T8) step; it keeps the structural theorem honest about comparing exactly the three mapped families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.