selectorTotalModels
plain-language theorem explainer
Fixes the GWTC-3 ringdown selector's total model-family count at 14. Anyone citing the family-stratified eligibility policy or the selector certificate uses this constant. It is a bare natural-number definition, not a derived theorem.
Claim. Under the GWTC-3 ringdown family-stratified likelihood selector, the total number of model families is $14$.
background
The module records a structural selector policy for future GWTC-3 ringdown likelihood work. It partitions HDF5 files and model families into eligible versus blocked sets; it does not evaluate any posterior.
Eligible families are the three with formalized observable maps: direct one-mode damping (DS_1mode_10M) and Kerr 220 quality-factor maps at 0M and 10M start. Everything else is blocked until a mapping is formalized (all Kerr_221*, all MMRDNP*, and pseobnrv4hm).
Sibling constants fix the complementary counts: 243 total files (66 eligible, 177 blocked) and 3 eligible / 11 blocked model families. This definition is the model-side total that those partitions must sum to.
proof idea
Definitional constant: the body is the numeral 14. No tactics, lemmas, or computation. Downstream partition theorems unfold this name and discharge equality by decide.
why it matters
Anchors the model-count side of the selector certificate. selector_model_count_partition proves eligible plus blocked models equal this total. The one-statement selector theorem packages selectorTotalModels = 14 with the file counts and eligibility claims. The certificate structure GWTC3RingdownLikelihoodSelectorCert requires the same partition as a field.
In the broader Verification domain this is bookkeeping for a future ringdown likelihood pipeline, not a Recognition forcing-chain step (T0–T8) or a mass/alpha derivation. It closes the structural count so later likelihood work cannot silently change the family inventory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.