selector_no_mixed_aggregation_true
plain-language theorem explainer
The GWTC-3 ringdown likelihood selector records an explicit policy flag that mixed aggregation across waveform families is forbidden, and that flag equals true. Anyone assembling or auditing the master selector certificate cites this equality. The proof is reflexivity on a Boolean constant defined as true.
Claim. The selector policy flag asserting that mixed aggregation of ringdown likelihoods across waveform families is disallowed evaluates to $\mathrm{true}$.
background
This module fixes the structural selector policy for future GWTC-3 ringdown likelihood work. It partitions HDF5 files and model families into eligible versus blocked sets: three mapped families (DS_1mode_10M, Kerr_220_0M, Kerr_220_10M) are eligible; Kerr 221, MMRDNP, and related families stay blocked until their observable mappings are formalized. Counts are fixed (243 files total, 66 eligible, 177 blocked; 14 model families, 3 eligible, 11 blocked).
The Boolean selectorNoMixedAggregation is the explicit policy bit that forbids pooling or averaging likelihoods across those strata. The module states it is selector policy only and computes no posterior. Upstream, the flag is defined as the constant true.
proof idea
One-line term proof by rfl. The definition of the no-mixed-aggregation flag is literally the Boolean constant true, so equality to true is definitional.
why it matters
The equality is a field-level witness inside the master certificate gwtc3RingdownLikelihoodSelectorCert, which packages file and model count partitions, eligible-file agreement with the family comparison layer, and total-file agreement with the filename taxonomy. Without a proved true flag, the certificate could not assert that the selector refuses mixed-family aggregation.
In the broader Verification domain this is structural hygiene for GWTC-3 ringdown work: it locks the policy that only the three mapped families may enter a stratified likelihood pipeline, and that blocked families must not be silently folded in. It does not touch the RS forcing chain (T0–T8), RCL, or mass ladder; it is an observational-data gate, not a derivation of constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.