selectorNoMixedAggregation
plain-language theorem explainer
Boolean policy flag fixed to true: GWTC-3 ringdown likelihood selection never aggregates eligible and blocked waveform families in one posterior. Verification and catalog auditors cite it when checking that the stratified selector stays pure. The body is the literal constant true; a companion theorem discharges equality by rfl.
Claim. The GWTC-3 ringdown likelihood selector policy flag asserting that eligible and blocked families are never mixed in a single aggregation is the Boolean value $\mathrm{true}$.
background
The module records 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_1mode_10M (direct $f_{t0}/\tau_{t0}$ damping), Kerr_220_0M, and Kerr_220_10M (Kerr 220 quality-factor maps at 0M and 10M start). Everything else is blocked until a mapping exists: all Kerr_221*, all MMRDNP*, and pseobnrv4hm.
Catalog arithmetic is fixed in companion constants: 243 total HDF5 files (66 eligible, 177 blocked) and 14 model families (3 eligible, 11 blocked). The present flag is the Boolean companion to that partition: it encodes the rule that likelihoods must not pool across the eligible/blocked cut.
proof idea
Definitional constant: the body is the Boolean literal true. No lemmas, tactics, or arithmetic are involved. Downstream, selector_no_mixed_aggregation_true proves equality to true by rfl.
why it matters
The flag is a field-level ingredient of the master certificate GWTC3RingdownLikelihoodSelectorCert and appears in the conjunctive one-statement theorem gwtc3_ringdown_likelihood_selector_one_statement, which packages file counts, model counts, partition identities, and this no-mix policy. Together they close the structural half of the GWTC-3 ringdown selector (module status: 0 sorry, 0 RS-internal axioms). The content is verification policy, not a forcing-chain step (T0–T8) or a mass/alpha derivation; it keeps future likelihood pipelines from silently mixing unmapped families into RS-facing ringdown tests.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.