dsFamilyEventCount
plain-language theorem explainer
Fixes the event count of the GWTC-3 controlled family DS_1mode_10M at 22. Anyone citing the family damping certificate or the one-statement pooled-interval theorem needs this constant. It is a bare Nat definition, not a derived count.
Claim. The number of distinct events in the GWTC-3 ringdown controlled family with model $\mathrm{DS\_1mode\_10M}$ is $N_{\mathrm{evt}} = 22$.
background
The module records a controlled-family scaling of the one-member QNM damping statistic on GWTC-3 ringdown posteriors. The family is locked to a single model name, DS_1mode_10M: 22 HDF5 files, 22 events, and 643624 pooled posterior samples. The observable is damping per cycle, $\exp(-1/(f_{t0}\tau_{t0}))$, compared against the RS target $1/\varphi \approx 0.618$.
Sibling constants fix the matching member count, total sample count, pooled mean/std/quantiles, and the RS damping target. This event-count constant is the Nat that those siblings and the certificate structure treat as the family size on the event axis. The module is structural only: it does not mix Kerr, MMRDNP, or other waveform-model semantics, and it is not a full-archive likelihood.
proof idea
Bare definition: the constant is the literal natural number 22. No lemmas, no tactics. Downstream positivity is discharged by unfold plus decide.
why it matters
Supplies the event-axis size used by three local consumers: the positivity lemma 0 < dsFamilyEventCount, the certificate structure field event_count_pos, and the one-statement controlled-family theorem that conjoins member count, event count, sample count, and containment of the RS target $1/\varphi$ inside the pooled 90% and 68% intervals.
In the broader Verification layer this is bookkeeping for the first controlled-family check that the ringdown damping-per-cycle posterior sits on the RS scale set by $\varphi$ (Berry threshold and related $\varphi$-ladder landmarks). It does not itself prove physics; it pins the $N=22$ figure so the certificate and one-statement theorem are fully grounded and sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.