comparisonTotalSamples
plain-language theorem explainer
Fixes the pooled posterior sample count across the three GWTC-3 ringdown damping families at 1,954,998. Anyone citing the controlled-family comparison certificate or the one-statement mean/median/hit-order theorem needs this constant. It is a bare Nat literal, not a derived computation.
Claim. The total number of posterior samples in the three-family GWTC-3 ringdown comparison is $N_{\mathrm{tot}}=1954998$, equal to the sum of the DS $1$-mode $10M$, Kerr $220$ $0M$, and Kerr $220$ $10M$ family sample counts.
background
The module compares three mapped GWTC-3 ringdown damping families: DS one-mode at $10M$, Kerr $(2,2,0)$ at $0M$, and Kerr $(2,2,0)$ at $10M$. It records structural orderings of pooled means, medians, and target-inclusion hit rates across those families only.
Each family contributes a fixed total sample count (posterior draws used in the pooled statistics). This definition names the arithmetic total of those three counts as a single natural number used by the comparison certificate and the one-statement theorem.
The setting is deliberately narrow: a three-family controlled comparison, not an archive-wide mixed-model likelihood. Status is structural (zero sorry, no new RS axioms).
proof idea
Definition by literal assignment: the constant is the natural number $1954998$. No tactic proof. Downstream, comparison_total_samples unfolds the three family totals and this constant, then closes equality by decide.
why it matters
Pins the sample-size side of the controlled-family ledger. The certificate structure GWTC3RingdownFamilyComparisonCert requires a field proving the three family sample counts sum to this constant. The one-statement theorem gwtc3_ringdown_family_comparison_one_statement conjoins comparisonTotalSamples = 1954998 with family count $3$, member total $66$, and the mean/median/hit-order facts.
Without a fixed total, the pooled mean and hit-rate comparisons would lack a named denominator. This is verification bookkeeping for GWTC-3 ringdown model/start-time dependence, not a Recognition forcing-chain step (T0–T8) or a mass/ladder claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.