selector_file_count_partition
plain-language theorem explainer
Eligible plus blocked GWTC-3 ringdown HDF5 files sum exactly to the catalog total: 66 + 177 = 243. Anyone citing the selector certificate or auditing the family-stratified likelihood policy needs this partition. The proof unfolds the three Nat constants and closes by decidable arithmetic.
Claim. The number of selector-eligible GWTC-3 ringdown HDF5 files plus the number of blocked files equals the total number of HDF5 files in the catalog: $66 + 177 = 243$.
background
This module fixes the selector policy for future GWTC-3 ringdown likelihoods. It does not compute posteriors; it only records which waveform families are mapped and which remain blocked. Eligible families are the three with formalized observable maps: DS_1mode_10M (direct $f_{t0}/\tau_{t0}$ damping), Kerr_220_0M, and Kerr_220_10M. Everything Kerr_221*, MMRDNP*, and pseobnrv4hm stays blocked until mappings exist.
Three Nat constants encode the file census: total HDF5 files = 243, eligible = 66, blocked = 177. Parallel constants track model-family counts (14 total, 3 eligible, 11 blocked). The partition identity is the file-level sanity check that eligible and blocked are complementary and exhaustive relative to the taxonomy total.
proof idea
Term-mode proof by unfolding the three definitions selectorEligibleFiles, selectorBlockedFiles, and selectorTotalHDF5Files to the literals 66, 177, and 243, then decide on the closed Nat equality $66 + 177 = 243$. No lemmas beyond decidable arithmetic.
why it matters
Feeds the certificate bundle gwtc3RingdownLikelihoodSelectorCert, which packages four structural facts (file partition, model partition, eligible-files match to the comparison module, total-files match to the taxonomy). Without this equality the certificate cannot assert that the selector is a clean bipartition of the HDF5 catalog.
In the Recognition verification layer this is pure bookkeeping: it locks the published counts (243 / 66 / 177) so downstream likelihood work cannot silently reclassify blocked families. It touches no forcing-chain step (T0–T8), no RCL identity, and no mass or alpha formula; it only closes the structural half of the GWTC-3 ringdown selector before any posterior is computed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.