gwtc3RingdownGuardedFamilyScriptsCert
plain-language theorem explainer
Packages the Session 133 operational guard into one certificate: eligible GWTC-3 ringdown family scripts pass the runtime model gate, a representative blocked model is rejected, smoke tests all pass, and the three mapped family certificates plus the guard certificate are inhabited. Verification authors cite it as the single inhabited witness that the Python family-statistic scripts are wired to the Lean guard. Construction is pure structure assembly from already-proved field lemmas.
Claim. There is a certificate recording that (i) the number of guarded scripts equals the number of guard-eligible models, (ii) every smoke test passes and the pass count equals the test count, (iii) the models $\mathrm{DS\_1mode\_10M}$, $\mathrm{Kerr\_220\_0M}$, and $\mathrm{Kerr\_220\_10M}$ are accepted by the runtime guard, (iv) a representative blocked model is rejected, and (v) the DS, Kerr $220\_0M$, Kerr $220\_10M$, and family-guard certificates are each inhabited.
background
This module is the Session 133 structural closure for GWTC-3 ringdown verification. Three mapped family-statistic scripts (DS 1-mode 10M damping, Kerr 220 0M damping, Kerr 220 10M damping) now call require_eligible_model before reading posterior data. The module states explicitly that this is operational guarding only: no new physics mapping and no new likelihood.
The certificate structure bundles ten fields. guardedScriptCount must equal guardEligibleModelCount. Smoke tests must all pass with matching counts. Three named models must evaluate to .accept under guardModel, and a representative blocked case must be rejected. Four upstream inhabited certificates must be available: the three family damping certificates and the runtime family-guard certificate.
Upstream one-liners already discharge the individual acceptances (guard_accepts_DS, guard_accepts_Kerr2200, guard_accepts_Kerr22010) and the count equality by rfl. The family and guard modules each expose a Nonempty witness theorem.
proof idea
Pure structure construction. Each field of GWTC3RingdownGuardedFamilyScriptsCert is filled by a named sibling or imported theorem: guarded_script_count_matches_selector for the count equality; smoke_all_passed and smoke_pass_count_eq_test_count for the smoke suite; guarded_DS_script_accepted, guarded_Kerr2200_script_accepted, and guarded_Kerr22010_script_accepted for the three acceptances; representative_blocked_rejected for the negative case; and the four *_Cert_inhabited theorems for availability of the DS, Kerr2200, Kerr22010, and family-guard certificates. No new reasoning occurs here.
why it matters
Feeds the one-statement inhabited theorem gwtc3RingdownGuardedFamilyScriptsCert_inhabited, which is the citation handle for "guarded family scripts are certified." In the Recognition verification stack this closes the operational loop between Lean eligibility predicates and the three Python GWTC-3 ringdown family scripts, so downstream audits can treat the guard wiring as a single Nonempty fact rather than a scatter of lemmas.
It does not advance the forcing chain (T0–T8), the Recognition Composition Law, or any mass/ladder claim. Its role is audit hygiene: zero sorry, zero new RS-specific axioms, and a dated structural closure (2026-05-22) that keeps family-statistic runs from silently reading posteriors for ineligible models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.