smokeTestCount
plain-language theorem explainer
Fixes the smoke-test suite size at seven cases for the GWTC-3 ringdown guarded-family scripts. Verification authors cite it when equating pass counts to the suite size or packaging the Session 133 certificate. The body is a bare natural-number constant, so equalities discharge by reflexivity.
Claim. The smoke-test suite for the GWTC-3 ringdown guarded family scripts has cardinality $7$.
background
This module closes Session 133 of the GWTC-3 ringdown verification stack. Three mapped family-statistic scripts (DS 1-mode 10M damping, Kerr 220 0M damping, Kerr 220 10M damping) now call a runtime eligibility guard before reading posterior data. The guard is operational only: it adds no new physics mapping and computes no new likelihood.
A smoke suite checks that eligible model labels are accepted and that representative blocked or unknown labels are rejected. Sibling constants record how many scripts are guarded, how many smoke cases pass, and whether the full suite passed. This definition is the fixed denominator of that suite: the number of smoke cases that must be exercised.
proof idea
Pure definitional constant: smokeTestCount is the natural number 7. There is no tactic proof. Downstream equalities such as pass-count equals test-count are closed by rfl once the pass counter is defined to match.
why it matters
Pins the suite size used by the one-statement theorem for guarded family scripts, which asserts among other conjuncts that the smoke-test count is 7, the pass count is 7, and the all-passed flag is true. The certificate structure GWTC3RingdownGuardedFamilyScriptsCert packages the same count equality. Together with the three acceptances of the mapped scripts and a representative blocked rejection, this constant makes the Session 133 structural claim machine-checkable: zero sorry, zero new RS-internal axioms, operational guarding only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.