selectorBlockedModels
plain-language theorem explainer
Records that eleven GWTC-3 ringdown model families are blocked from the likelihood selector. Anyone citing the family-stratified GWTC-3 policy or the model-count partition uses this constant. It is a bare natural-number definition fixed by the module's selector policy, not a derived count.
Claim. Under the GWTC-3 ringdown family-stratified likelihood selector, the number of blocked model families is $11$.
background
The module fixes a structural selector policy for future GWTC-3 ringdown likelihood work. It does not evaluate posteriors. Mapped (eligible) families are the three with formalized observable maps: direct $f_{t0}/\tau_{t0}$ damping (DS_1mode_10M) and Kerr-220 quality-factor maps at $0M$ and $10M$ start times. Everything else is blocked until a mapping is formalized: all Kerr_221* families, all MMRDNP* families, and pseobnrv4hm.
Alongside file counts (243 total HDF5, 66 eligible, 177 blocked), the policy records model-family counts: 14 total, 3 eligible, 11 blocked. This declaration is the blocked-model leg of that triple. Sibling constants hold the eligible and total model counts; partition lemmas assert they add correctly.
proof idea
No proof. The declaration is a definition equal to the natural number 11, matching the blocked-family tally stated in the module policy. Downstream theorems unfold it and discharge equalities by simp or decide.
why it matters
Gives the blocked side of the model-count ledger that the selector certificate and the one-statement selector theorem quote. selector_model_count_partition uses it to prove eligible plus blocked equals total models (3 + 11 = 14). GWTC3RingdownLikelihoodSelectorCert packages that partition. The family-guard layer equates its own blocked-model count to this constant via guard_counts_match_selector, so guard and selector stay synchronized.
In the broader Verification domain this is policy bookkeeping only: it freezes which waveform families may enter a future ringdown likelihood until 221-mode, MMRDNP, and pseobnr mappings exist. It does not touch RS forcing (T0–T8), the J-cost, or mass-ladder claims; it is an empirical-data gate for GWTC-3 ringdown comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.