GWTC3RingdownGuardedFamilyScriptsCert
plain-language theorem explainer
Certificate bundle asserting that the three GWTC-3 ringdown family-statistic scripts are runtime-guarded: guarded script count matches the three eligible models, smoke tests all pass, the DS and two Kerr-220 families are accepted while three blocked models are rejected, and the underlying family and guard certificates are inhabited. Downstream one-statement and shared-runner certificates cite it. Pure structure packing equalities and Nonempty witnesses; no proof body.
Claim. A certificate packing eleven assertions: the number of guarded scripts equals the number of guard-eligible models; every smoke test passes and the pass count equals the test count; the guard accepts $\mathrm{DS\_1mode\_10M}$, $\mathrm{Kerr\_220\_0M}$, and $\mathrm{Kerr\_220\_10M}$; it rejects $\mathrm{Kerr\_221\_0M}$, $\mathrm{MMRDNP\_10M}$, and $\mathrm{pseobnrv4hm}$; and the DS, Kerr $220$ $0M$, Kerr $220$ $10M$, and family-guard certificates are each inhabited.
background
Session 133 of the GWTC-3 ringdown verification stack wires a runtime family guard into the three mapped family-statistic scripts (damped-sinusoid 1-mode 10M, Kerr 220 0M, Kerr 220 10M). Each script must call an eligibility check before reading posterior data. The module is operational guarding only: no new physics mapping and no new likelihood.
The guard itself is a pure string classifier: three named models are accepted and every other name is rejected. Eligible-model count is fixed at 3, matching the three patched scripts. Upstream family certificates already record taxonomy membership, positive event and sample counts, and target-inside-pooled-90% for each accepted family; the family-guard certificate records the accept/reject table.
This structure is the single place that ties script-level smoke results, the guard decision table, and inhabitance of those upstream certificates into one record.
proof idea
No proof body: the declaration is a structure (certificate type). Each field is a Prop-valued requirement. Inhabitation is supplied downstream by a concrete value that fills every field from sibling lemmas: count equality from the selector match, smoke flags from the Boolean constants, accept/reject decisions from the guard definition by case split on the model string, and Nonempty witnesses from the existing family and guard certificate values.
why it matters
Closes the Session 133 structural theorem (0 sorry, 0 new RS axioms): the runtime guard is now certified as wired into the three family scripts. The inhabited instance and the one-statement conjunction theorem are built directly from this structure; the shared-runner certificate further requires that the refactored family-script count equal the guarded-script count recorded here. Within the Recognition verification domain this is infrastructure hygiene, not a forcing-chain step (T0-T8) or a mass/alpha claim: it prevents unmapped or blocked ringdown families from silently entering the GWTC-3 statistic pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.