guarded_Kerr22010_script_accepted
plain-language theorem explainer
The GWTC-3 ringdown family guard accepts the Kerr 220 mode with 10M damping as an eligible model string. Verification authors wiring the mapped family-statistic scripts cite this to lock that gate. Proof is a one-line wrapper of the corresponding guard-accept lemma.
Claim. The ringdown family guard returns $\mathrm{accept}$ on the model identifier $\mathrm{Kerr\_220\_10M}$.
background
This module is Session 133 structural closure: the runtime family guard is wired into the three mapped GWTC-3 ringdown family-statistic scripts. Each script must call an eligibility check before reading posterior data. The guard is operational only; it adds no physics mapping and computes no likelihood.
The guard is a string-case decision on three hard-coded eligible families: the DS one-mode 10M damping family, the Kerr 220 mode at 0M damping, and the Kerr 220 mode at 10M damping. Every other string is rejected. Upstream, the same equality is already proved by unfolding that decision and simplifying.
proof idea
One-line wrapper: the proof is exactly the upstream theorem that the guard accepts $\mathrm{Kerr_220_10M}$. That upstream result unfolds the guard definition and discharges the matching branch by simplification.
why it matters
Feeds the module certificate gwtc3RingdownGuardedFamilyScriptsCert, which packages guarded-script count, smoke-test passage, and the three accepted-family lemmas (DS, Kerr 220 0M, Kerr 220 10M). Together they certify that eligible families pass the gate and representative blocked families fail, with zero sorry and no new RS axioms. This is verification plumbing for GWTC-3 ringdown family scripts, not a step in the T0–T8 forcing chain or a mass/alpha claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.