dsFamilyTotalSampleCount
plain-language theorem explainer
The DS_1mode_10M controlled family pools 643,624 posterior samples of the ringdown damping-per-cycle observable across 22 GWTC-3 events. Anyone citing the family certificate, the one-statement damping theorem, or the multi-family sample total needs this exact count. It is a literal natural-number constant, discharged by definitional unfolding and decide.
Claim. The total number of pooled posterior samples in the GWTC-3 ringdown family with model $\mathrm{DS\_1mode\_10M}$ is the natural number $643624$.
background
The module records a controlled-family scaling of the Session 123 one-member QNM damping statistic for the damped-sinusoid model DS_1mode_10M. The family comprises 22 HDF5 files and 22 events; the observable is damping per cycle, $\exp(-1/(f_{t_0}\tau_{t_0}))$, compared against the RS target $1/\varphi\approx 0.618$.
Sibling constants fix the rest of the census: member count 22, event count 22, and the pooled mean, std, median, and quantile ladder of the damping samples. The module status is structural theorem: zero sorry and zero new RS-specific axioms. This constant is only the sample-size anchor for those statistics; it does not encode Kerr or MMRDNP semantics.
proof idea
Pure definitional constant: the right-hand side is the numeral 643624. Downstream positivity and equality proofs unfold the name and finish with decide. No lemmas are required at the definition site itself.
why it matters
The count is the sample-size field of the family certificate and appears explicitly in the one-statement controlled-family damping theorem (member count 22, event count 22, sample count 643624, target inside the pooled 90% and 68% intervals). Family comparison adds it to the Kerr 2200 and Kerr 22010 totals to obtain the multi-family sample sum and the corresponding comparison certificate.
In the Recognition verification layer this pins the empirical weight behind the claim that $1/\varphi$ sits inside the pooled damping intervals for a single, non-mixed waveform family. It does not close a forcing-chain step (T0–T8); it is archive-side evidence that the RS damping target is not excluded by this controlled GWTC-3 slice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.