selector_eligible_files_match_comparison
plain-language theorem explainer
The GWTC-3 ringdown selector's eligible-file count equals the family-comparison total-member count: both are the natural number 66. Anyone auditing consistency between the likelihood selector and the comparison census cites this equality. The proof is pure reflexivity on two constant definitions.
Claim. The number of HDF5 files marked eligible by the GWTC-3 ringdown likelihood selector equals the total member count used in the ringdown family comparison: both equal $66$.
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 (Kerr 221, MMRDNP, pseobnrv4hm, and related) is blocked until a mapping is written down.
Two independent Nat constants record the eligible-file census: the selector's eligible-file count and the comparison module's total-member count. Both are hard-coded to 66 against a taxonomy of 243 total HDF5 files (177 blocked). The surrounding certificate also partitions model families (3 eligible of 14).
proof idea
One-line reflexivity. Both sides reduce definitionally to the same natural-number literal 66, so rfl closes the goal with no lemmas and no rewriting.
why it matters
The equality is one of four fields packed into gwtc3RingdownLikelihoodSelectorCert, the module's closure certificate. That certificate also records the file-count and model-count partitions and the match of total files against the filename taxonomy. Together they pin the selector policy as a zero-sorry, zero-new-axiom structural theorem: eligible counts used downstream for likelihood selection cannot silently drift from the comparison census. This is verification scaffolding only; it does not touch the RS forcing chain (T0–T8), RCL, or mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.