selectorEligibleFiles
plain-language theorem explainer
Fixes the count of GWTC-3 ringdown HDF5 files admitted by the family-stratified likelihood selector at 66. Anyone citing the selector certificate or the one-statement count theorem uses this constant. It is a bare natural-number definition, not a derived computation.
Claim. The number of GWTC-3 ringdown HDF5 files eligible under the family-stratified likelihood selector is $66$.
background
The module records selector policy for future GWTC-3 ringdown likelihood analyses. It does not evaluate posteriors. Eligible families are those with a formalized observable map: the direct one-mode damping family DS_1mode_10M, and the Kerr 220 quality-factor families at start times 0M and 10M. All Kerr 221, MMRDNP, and pseobnrv4hm families remain blocked until their mappings are formalized.
Catalog totals stated in the module header are 243 HDF5 files and 14 model families, of which 66 files and 3 families are eligible. Companion constants fix the blocked and total counts so that partition identities can be checked by decide.
proof idea
No proof. The declaration is a definitional constant equal to the natural number 66. Downstream equalities unfold it and discharge arithmetic by rfl or decide.
why it matters
This constant is the eligible-file side of the selector ledger. It appears in the certificate structure GWTC3RingdownLikelihoodSelectorCert (file-count partition and eligible-files-match-comparison fields), in the one-statement selector theorem that packages all six catalog numbers, and in the partition and comparison lemmas that equate it to the blocked/total split and to the comparison-module member count. Within Recognition Science verification it freezes the admission policy before any likelihood is computed, so later ringdown tests cannot silently enlarge the sample. It is structural bookkeeping only; it does not touch the forcing chain, RCL, or mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.