selectorEligibleModels
plain-language theorem explainer
Records that exactly three GWTC-3 ringdown model families are eligible under the stratified likelihood selector: the direct one-mode damping map and the two Kerr-220 quality-factor maps. Downstream guard and certificate theorems cite this constant to pin the eligible-model count. It is a bare natural-number definition, not a derived count.
Claim. The number of GWTC-3 ringdown model families admitted by the likelihood selector is $3$ (namely the direct $f_{t_0}/\tau_{t_0}$ one-mode family and the Kerr $220$ quality-factor families at $0M$ and $10M$ start).
background
The module fixes a structural selector policy for future GWTC-3 ringdown likelihood work. It does not evaluate posteriors; it only partitions the catalog into mapped (eligible) and unmapped (blocked) families so that later certificates can quote fixed counts.
Eligible families are those with a formalized observable map: direct damping parameters $f_{t_0}/\tau_{t_0}$ for DS_1mode_10M, and Kerr-220 quality-factor maps at start times $0M$ and $10M$. Everything else in the taxonomy (all Kerr-221 variants, MMRDNP families, and pseobnrv4hm) stays blocked until a mapping is written down.
Sibling constants record the rest of the partition: 14 total model families, 11 blocked, and the parallel file-level counts 243 / 66 / 177. This definition is the eligible-model half of that ledger.
proof idea
No proof. The declaration is a definitional constant equal to the natural number 3, matching the three named eligible families in the module policy. Downstream theorems unfold it and discharge equalities by simp or decide.
why it matters
This constant is the eligible-model side of the selector ledger. The partition theorem selector_model_count_partition uses it to prove eligible plus blocked equals total models. The one-statement selector theorem packages selectorEligibleModels = 3 with the file and total-model counts. The certificate structure GWTC3RingdownLikelihoodSelectorCert requires the same model-count partition as a field. On the guard side, guard_counts_match_selector equates the guard's eligible-model count to this constant, and the guard certificate lists the three accepted family names that justify the count of three.
In the broader Verification domain this is pure catalog hygiene: it freezes which ringdown families may enter a future likelihood comparison so that RS claims about GWTC-3 ringdowns cannot silently mix unmapped waveforms. It touches no forcing-chain landmark (T0–T8), no RCL identity, and no mass or coupling constant; it only gates empirical input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.