guarded_script_count_matches_selector
plain-language theorem explainer
The count of runtime-guarded GWTC-3 ringdown family scripts equals the count of models marked eligible by the family guard; both are three. Verification authors cite this when assembling the guarded-scripts certificate. The proof is definitional equality by reflexivity.
Claim. The number of guarded GWTC-3 ringdown family scripts equals the number of models eligible under the ringdown family guard: both equal $3$.
background
This module is Session 133 of the GWTC-3 ringdown verification stack. It wires the runtime family guard into three mapped family-statistic scripts (DS1 mode-1 0M damping, Kerr 220 0M damping, Kerr 220 10M damping). Each script must call the eligibility check before reading posterior data.
Two natural-number constants record the same inventory from different sides: the script-side count of guarded families, and the guard-side count of eligible models. Both are hard-coded to three. The module is operational guarding only: no new physics mapping and no new likelihood.
proof idea
One-line reflexivity. Both sides reduce by unfolding to the numeral $3$, so rfl closes the equality.
why it matters
Feeds the guarded_count field of the module certificate gwtc3RingdownGuardedFamilyScriptsCert, which packages count match, smoke-test pass, and per-script acceptance lemmas. That certificate is the structural closure that the three patched Python family scripts are aligned with the Lean eligibility selector. It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it is pure verification hygiene for GWTC-3 ringdown family statistics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.