selector_total_files_match_taxonomy
plain-language theorem explainer
The GWTC-3 ringdown selector's total HDF5 file count equals the filename taxonomy's total (both 243). Anyone auditing the selector certificate against the taxonomy inventory cites this equality. The proof is definitional reflexivity: both sides reduce to the same natural number literal.
Claim. The selector's total number of GWTC-3 ringdown HDF5 files equals the taxonomy inventory count: both are $243$.
background
The module records a structural selector policy for future GWTC-3 ringdown likelihoods. It partitions model families into eligible ones (DS_1mode_10M, Kerr_220_0M, Kerr_220_10M) and blocked ones (all Kerr_221*, MMRDNP*, and pseobnrv4hm until mappings are formalized). It computes no posterior; it only freezes counts and eligibility.
Two independent Nat constants both equal 243: the taxonomy inventory total (taxonomyHDF5FileCount) and the selector's declared total (selectorTotalHDF5Files). The taxonomy side is the filename census; the selector side is the policy's own bookkeeping. Aligning them is a consistency check before the certificate packages partition and eligibility lemmas.
proof idea
One-line definitional equality via rfl. Both selectorTotalHDF5Files and taxonomyHDF5FileCount are defined as the literal 243, so the equality holds by reduction with no lemmas or case analysis.
why it matters
Feeds the field total_files_match_taxonomy of gwtc3RingdownLikelihoodSelectorCert, the packaged certificate that the selector's file and model partitions, eligible-file comparison, and taxonomy total are all consistent. Without this equality, the certificate could claim a different universe of files than the taxonomy module. In the Recognition verification layer this is bookkeeping hygiene for GWTC-3 ringdown family stratification, not a physics derivation from the forcing chain; it locks the 243-file census so later likelihood work cannot silently change the sample size.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.