smokePassCount
plain-language theorem explainer
Records that seven smoke tests of the GWTC-3 ringdown guarded family scripts all pass, as the constant natural number 7. Verification authors cite it when packaging the Session 133 guard wiring into a single certificate. The body is a bare numeric definition, equated to the test count by reflexivity.
Claim. The number of passed smoke tests for the GWTC-3 ringdown guarded family scripts is the natural number $7$.
background
Session 133 wires the runtime family guard into three mapped GWTC-3 ringdown family-statistic scripts (DS 1-mode 10M damping, Kerr 220 0M damping, Kerr 220 10M damping). Each script must call require_eligible_model before reading posterior data. The module is operational guarding only: no new physics mapping and no new likelihood.
Smoke tests check that eligible model families are accepted and that representative blocked or unknown families are rejected. Sibling constants fix the guarded-script count at three and the total smoke-test count at seven. This definition is the matching pass count.
proof idea
Numeric definition: the constant is set equal to 7 with no proof obligations. Downstream, equality with the smoke-test count is immediate by rfl.
why it matters
Feeds the certificate structure GWTC3RingdownGuardedFamilyScriptsCert (field requiring the smoke pass count) and the one-statement theorem that packages guarded-script count, smoke counts, all-passed flag, and accept/reject outcomes for the three mapped models plus a blocked representative. Together with smoke_pass_count_eq_test_count, it closes the smoke half of the structural theorem (0 sorry, 0 new RS axioms). It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it only certifies that the guard is live in the verification scripts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.