representative_blocked_rejected
plain-language theorem explainer
Three representative blocked GWTC-3 ringdown model tags (Kerr 221 0M, MMRDNP 10M, and pseobnrv4hm) are each rejected by the runtime family guard. Verification authors cite this when certifying that smoke tests fail on ineligible families. The proof is a one-line product of the three individual rejection lemmas.
Claim. The family guard returns reject on each of the strings $\mathrm{Kerr\_221\_0M}$, $\mathrm{MMRDNP\_10M}$, and $\mathrm{pseobnrv4hm}$.
background
Session 133 wires a runtime family guard into the mapped GWTC-3 ringdown family-statistic scripts. The guard is a pure string classifier: it accepts only three eligible model tags (DS 1-mode 10M, Kerr 220 0M, Kerr 220 10M) and rejects every other string. Operational guarding only; no new physics mapping or likelihood is computed.
The three tags named here are the representative blocked or unknown families used in the smoke suite. Upstream, each rejection is already proved by unfolding the guard definition and simplifying the string comparisons. This declaration simply packages those three facts as a single conjunction for the master certificate.
proof idea
Term-mode product introduction. The proof is the triple of upstream lemmas guard_rejects_Kerr2210, guard_rejects_MMRDNP, and guard_rejects_pseobnrv4hm. Each of those unfolds guardModel and closes by simp on the string inequalities against the three accept branches. No further reasoning is needed here.
why it matters
Feeds the master certificate gwtc3RingdownGuardedFamilyScriptsCert, which bundles guarded-script counts, smoke-pass facts, and the three accepted-family scripts. Together with the accepted-script lemmas, this shows the smoke suite both passes eligible families and fails representative blocked ones, closing the operational-guarding claim of the module (structural theorem, zero sorry, zero new RS axioms).
It does not touch the Recognition forcing chain (T0–T8), RCL, or mass ladder; it is pure verification plumbing for GWTC-3 ringdown family scripts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.