selectorTotalHDF5Files
plain-language theorem explainer
Fixes the GWTC-3 ringdown catalog size at 243 HDF5 files for the family-stratified likelihood selector. Anyone citing the eligible/blocked partition or the one-statement selector certificate uses this constant. It is a bare natural-number definition, not a derived count.
Claim. The total number of GWTC-3 ringdown HDF5 files under the selector policy is the natural number $243$.
background
The module records selector policy for future GWTC-3 ringdown likelihoods. It does not compute posteriors. Mapped (eligible) families are the direct damping map DS_1mode_10M and the two Kerr-220 quality-factor maps at 0M and 10M start; all Kerr-221, MMRDNP, and pseobnrv4hm families stay blocked until their observable maps are formalized.
Catalog arithmetic is stated in fixed naturals: 243 total HDF5 files, 66 eligible, 177 blocked; 14 model families with 3 eligible and 11 blocked. A companion taxonomy constant supplies the same total file count, so the selector and the filename taxonomy stay synchronized by definitional equality.
proof idea
No proof. The declaration is a definitional constant: the natural number 243 is assigned directly. Downstream partition and taxonomy-match theorems unfold this name and close by decide or rfl.
why it matters
This constant is the right-hand side of the file-count partition (eligible plus blocked equals total) and of the taxonomy match that identifies the selector total with the taxonomy HDF5 file count. It appears in the selector certificate structure and in the one-statement selector theorem that packages all six catalog numbers. Within Recognition Science verification it anchors the GWTC-3 ringdown gate: only the three formalized families may enter likelihood work; the remaining eleven stay out until mappings exist. It is policy bookkeeping, not a physics derivation from the forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.