comparison_total_samples
plain-language theorem explainer
The three GWTC-3 ringdown damping-family sample counts sum exactly to the comparison aggregate total 1,954,998. Anyone citing the three-family comparison certificate needs this bookkeeping identity. The proof unfolds the four Nat constants and closes by decidable arithmetic.
Claim. The DS 1-mode 10M family sample count plus the Kerr 220 0M family sample count plus the Kerr 220 10M family sample count equals the comparison total sample count: $643624 + 647220 + 664154 = 1954998$.
background
This module aggregates three mapped GWTC-3 ringdown damping families (DS 1-mode 10M, Kerr 220 0M, Kerr 220 10M) and proves model/start-time dependence on means, medians, and target inclusion. It is a three-family comparison only, not a mixed-model archive-wide likelihood. Status: structural theorem, zero sorry, zero new RS-specific axioms.
Each family exports a frozen Nat sample census: 643624 (DS), 647220 (Kerr 0M), 664154 (Kerr 10M). The comparison layer defines the aggregate total as 1954998. These are mapped posterior-sample counts, not RS-derived parameters.
The claim checked here is pure bookkeeping: the three family totals sum to the declared comparison total.
proof idea
Tactic proof by unfolding the four Nat definitions (DS family total, Kerr 220 0M total, Kerr 220 10M total, and the comparison aggregate), then decide on the resulting closed natural-number equation. No intermediate lemmas; pure definitional reduction plus decidable arithmetic.
why it matters
The GWTC-3 ringdown family comparison certificate installs this identity as its total-samples field, together with total members, mean order, and median order. Downstream readers of that certificate get machine-checked sample-size bookkeeping rather than an asserted constant.
On the Recognition Science verification side, the module closes a structural three-family ringdown comparison against GWTC-3. It sits outside the forcing chain (T0-T8), the Recognition Composition Law, and the phi-ladder mass formula; it is empirical-side verification now fully proved.
The parent certificate is the natural citation point when reporting ordered means/medians and target-inclusion degradation across DS 1-mode 10M, Kerr 220 0M, and Kerr 220 10M.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.