comparisonTotalMembers
plain-language theorem explainer
Fixes the pooled GWTC-3 ringdown member count at 66 across the three controlled damping families (DS 1-mode 10M, Kerr 220 0M, Kerr 220 10M). Downstream comparison and likelihood-selector certificates cite this constant so family sizes stay synchronized. It is a bare natural-number definition, discharged by `decide` or `rfl` at use sites.
Claim. The total number of GWTC-3 ringdown events retained in the three-family controlled comparison is the natural number $66$.
background
The module aggregates three mapped GWTC-3 ringdown damping families: DS one-mode at 10M start time, Kerr $(2,2,0)$ at 0M, and Kerr $(2,2,0)$ at 10M. It proves structural ordering facts on pooled means, medians, and target-inclusion bands, not a mixed-model archive-wide likelihood.
Each family exports its own member count. This definition names their sum as a single constant so certificates and one-statement theorems can refer to a fixed total rather than recomputing the arithmetic inline. The module status is structural: zero sorry, zero new RS-specific axioms.
proof idea
No proof body: a definitional binding of a natural number to $66$. Downstream theorems such as comparison_total_members unfold the three family counts together with this constant and close by decide; the likelihood selector equates eligible files to this constant by rfl.
why it matters
Anchors the three-family comparison certificate and the one-statement theorem, which assert that the total member count equals $66$ alongside family count $3$, sample total, mean/median orderings, and hit-band degradation. The likelihood-selector certificate reuses the same constant so eligible HDF5 files match the comparison pool exactly.
Within Recognition Science verification, this is bookkeeping for controlled GWTC-3 ringdown checks, not a forcing-chain step (T0–T8). It keeps the structural comparison reproducible and prevents silent drift between family modules and selector filters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.