gwtc3_ringdown_guarded_family_scripts_one_statement
plain-language theorem explainer
Packages the GWTC-3 ringdown guarded-family-script audit into one conjunction: three eligible models are accepted, seven smoke tests all pass, and the certificate structure is inhabited. Verification engineers closing Session 133 cite this as the single entry point. The proof is a term-mode conjunction of reflexivity on the numeric constants, three upstream guard-acceptance lemmas, and certificate inhabitation.
Claim. The guarded family-script count equals $3$; the smoke-test count and pass count both equal $7$ with every smoke test passing; the runtime family guard accepts the three eligible models $\mathrm{DS}_{1\mathrm{mode},10M}$, $\mathrm{Kerr}_{220,0M}$, and $\mathrm{Kerr}_{220,10M}$; and the guarded-family-scripts certificate is inhabited.
background
This module records Session 133 of the GWTC-3 ringdown verification stack. Three mapped family-statistic scripts (DS one-mode 10M damping, Kerr 220 at 0M, Kerr 220 at 10M) now call a runtime eligibility check before reading posterior data. The check is operational only: it adds no new physics mapping and computes no new likelihood.
The runtime decision is guardModel, a string-keyed table that accepts exactly those three model names and rejects everything else. Upstream lemmas guard_accepts_DS, guard_accepts_Kerr2200, and guard_accepts_Kerr22010 discharge the three accept cases by unfolding and simplifying that table. Sibling constants fix the guarded-script count at 3 and record a seven-case smoke suite that must all pass.
The certificate structure bundles the count match against the eligible-model tally, full smoke passage, and the three accept equalities into a single inhabited record used as the closure witness.
proof idea
Term-mode proof building an eight-way conjunction. The four numeric and Boolean equalities (guardedScriptCount = 3, smoke counts both 7, smokeAllPassed = true) are discharged by rfl against the in-module definitions. The three guard decisions are the upstream theorems guard_accepts_DS, guard_accepts_Kerr2200, and guard_accepts_Kerr22010. Inhabitation of the certificate structure is the sibling lemma gwtc3RingdownGuardedFamilyScriptsCert_inhabited. No tactics beyond the term constructor.
why it matters
Closes Session 133 as a structural theorem: zero sorry, zero new RS-internal axioms. It is the one-statement audit that the three patched family scripts are wired through the runtime guard and that the smoke suite confirms eligible families pass while blocked or unknown families fail. Downstream consumers are not yet wired (used_by is empty); the declaration itself is the terminal packaging of the guarded-script certificate.
Within Recognition Science this sits in the Verification domain, not the forcing chain (T0–T8) or the mass/ladder layer. It does not touch J-cost, RCL, phi, the eight-tick octave, or the alpha band. Its value is operational hygiene: mapped GWTC-3 ringdown family statistics cannot silently run on ineligible models once the guard is required.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.