selectorBlockedFiles
plain-language theorem explainer
Records the fixed count of GWTC-3 ringdown HDF5 files excluded by the family-stratified likelihood selector: 177. Anyone citing the selector partition or the one-statement selector theorem uses this constant. It is a bare natural-number definition, not a derived claim.
Claim. The number of blocked GWTC-3 ringdown HDF5 files under the family-stratified likelihood selector policy is $177$.
background
The module fixes a structural selector policy for future GWTC-3 ringdown likelihood work. It does not evaluate posteriors. Eligible families are the three with formalized observable maps: DS one-mode at 10M, Kerr 220 at 0M, and Kerr 220 at 10M. Everything else is blocked until a mapping exists: all Kerr 221 families, all MMRDNP families, and pseobnrv4hm.
Catalog counts are frozen as named naturals: 243 total HDF5 files, 66 eligible, 177 blocked; 14 model families total, 3 eligible, 11 blocked. The blocked-file count is the complement of the eligible set inside the taxonomy total.
proof idea
No proof. The declaration is a definition equating the blocked-file count to the literal natural 177. Downstream partition lemmas unfold this constant and discharge equalities by decide.
why it matters
Supplies the blocked side of the file-count partition used by selector_file_count_partition and by the certificate structure GWTC3RingdownLikelihoodSelectorCert. It appears in the conjunctive one-statement selector theorem and in the positivity fact that the blocked set is nonempty. Within Recognition verification this is bookkeeping only: it locks the exclusion policy so later likelihood comparisons cannot silently mix unmapped waveform families. It does not touch the forcing chain, RCL, or mass ladder; it is GWTC-3 data hygiene for ringdown tests.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.