guarded_Kerr2200_script_accepted
plain-language theorem explainer
The Kerr 220-mode, zero-mass-damping ringdown family is accepted by the GWTC-3 runtime family guard. Anyone wiring the Kerr_220_0M damping-family script into the guarded pipeline cites this. The proof is a one-line wrapper of the upstream acceptance lemma for that model string.
Claim. The runtime family guard returns accept on the model label $\mathrm{Kerr\_220\_0M}$ (Kerr ringdown, $\ell=m=2$, $n=0$ overtone, start time $0M$).
background
Session 133 wires a runtime family guard into the mapped GWTC-3 ringdown family-statistic scripts. Before any posterior is read, each script calls a model-eligibility check so only three named families proceed: the single-mode DS family at $10M$, and the two Kerr 220 families at $0M$ and $10M$ start times.
The guard is a pure string decision: on the three eligible labels it returns accept; on every other label it returns reject. No likelihood is recomputed and no new physics map is introduced. The upstream lemma already records that the Kerr $220$ zero-mass-damping label is one of the three accepted strings.
proof idea
One-line wrapper: the goal is definitionally the statement of guard_accepts_Kerr2200, which unfolds the guard and discharges the matching branch by simplification. No extra case analysis is performed here.
why it matters
Feeds the module certificate gwtc3RingdownGuardedFamilyScriptsCert, which bundles guarded-script count, smoke-test passage, and the three accepted-family lemmas (DS, Kerr $220$ at $0M$, Kerr $220$ at $10M$). Without this fact the Kerr $0M$ script cannot be certified as guard-eligible. The result is operational only: it closes the Session 133 structural theorem (zero sorry, zero new RS axioms) that the patched Python family scripts refuse blocked or unknown models before touching posteriors. It does not touch the forcing chain, RCL, or mass ladder; it only hardens the GWTC-3 verification surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.