guardedScriptCount
plain-language theorem explainer
Fixes the number of GWTC-3 ringdown family scripts under the runtime eligibility guard at three. Verification authors cite it when equating script inventory to the eligible-model selector and when packing the guarded-scripts certificate. The body is a literal natural-number definition, not a derived count.
Claim. The number of GWTC-3 ringdown family-statistic scripts that call the runtime eligibility guard is exactly $3$.
background
The module records Session 133 of the GWTC-3 ringdown verification stack: wiring the runtime family guard into the mapped family-statistic scripts. Three Python 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 this is operational guarding only: no new physics mapping and no new likelihood.
guardedScriptCount is the Lean-side inventory constant for those three patched scripts. Downstream equalities identify it with the count of models the guard accepts, and with the refactored shared-runner script count, so the certificate layer can assert inventory consistency by reflexivity.
proof idea
Definitional constant: the natural number three, with no proof obligations. Downstream theorems such as guarded_script_count_matches_selector and refactored_count_matches_guarded_count discharge equalities to other counts by rfl.
why it matters
Anchors the guarded-scripts certificate and the one-statement theorem for this module: both require the guarded count to equal three (and to match the eligible-model selector). The shared-runner certificate reuses it so the refactored family-script count equals the guarded inventory. Together these close the structural claim that the three patched ringdown scripts are exactly the guard-eligible set, with smoke tests confirming accept/reject behavior. No RS forcing-chain landmark (T0–T8, RCL, phi ladder) is involved; this is verification bookkeeping for GWTC-3 ringdown family statistics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.