guard_counts_match_selector
plain-language theorem explainer
The GWTC-3 ringdown family guard and the Session 131 likelihood selector agree on census: three eligible model families and eleven blocked ones. Anyone wiring the runtime guard certificate to the selector should cite this equality. The proof unfolds the four Nat constants and closes by simplification.
Claim. The guard's eligible-model count equals the selector's eligible-model count, and the guard's blocked-model count equals the selector's blocked-model count: both sides are $3$ eligible and $11$ blocked.
background
This module formalizes the runtime family guard induced by the Session 131 family-stratified likelihood selector for GWTC-3 ringdown analyses. The guard is pure policy: it accepts only three mapped families (DS one-mode 10M, Kerr 220 at 0M, Kerr 220 at 10M) and rejects blocked or unknown families (including Kerr 221, MMRDNP, pseobnrv4hm, and unknowns). It computes no posterior likelihood.
The four quantities compared here are bare natural-number constants. On the guard side, the eligible count is defined as 3 and the blocked count as 11. On the selector side, the eligible and blocked model counts are likewise 3 and 11. The theorem asserts that these two pairs of constants coincide, so the guard's census is locked to the selector's census.
proof idea
One-line style reduction: unfold the four definitions guardEligibleModelCount, guardBlockedModelCount, selectorEligibleModels, and selectorBlockedModels (each a literal Nat), then simp discharges the two equalities $3 = 3$ and $11 = 11$. No lemmas beyond definitional unfolding are required.
why it matters
The equality feeds the packaged certificate gwtc3RingdownFamilyGuardCert, which bundles accept/reject lemmas for the three allowed families and the blocked representatives. Without matching counts, the certificate could claim a different family inventory than the selector that induced the policy.
In the Recognition verification layer this is structural bookkeeping, not a physics derivation: it pins the runtime guard to the Session 131 selector so downstream checks cannot silently drift. It does not touch the forcing chain (T0–T8), RCL, or mass-ladder landmarks; its role is audit closure for GWTC-3 ringdown family policy (status: structural theorem, zero sorry, zero new RS axioms).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.