smokePassesAfterRefactor
plain-language theorem explainer
Records that seven smoke tests pass after the GWTC-3 ringdown guarded-family scripts were moved onto a shared runner. Verification authors cite it as the numeric pass count in the shared-runner certificate and the one-statement closure theorem. It is a bare natural-number definition, equal by reflexivity to the expected test count.
Claim. The post-refactor smoke-pass count is the natural number $7$.
background
The module freezes a structural refactor of GWTC-3 ringdown controlled-family damping scripts onto one shared guarded runner. That runner calls require_eligible_model before any posterior bytes are read and exposes two mapping labels: direct (damped-sinusoid $f_{t_0}/\tau_{t_0}$) and kerr220 (Kerr 220 $Q(a)$). The module states explicitly that this is a safety invariant only: no new physics mapping and no posterior likelihood.
Sibling constants track presence of the shared runner, how many family scripts were refactored, and how many mapping labels are supported. The smoke layer pairs an expected test count with this pass count so that equality can be checked by definitional reflexivity after the refactor.
proof idea
No proof. The declaration is a one-line definition binding a natural number to the literal $7$. Downstream, smoke_after_refactor_all_passed closes the equality with the expected smoke-test count by rfl.
why it matters
Feeds three local consumers: the equality theorem smoke_after_refactor_all_passed, the structure GWTC3RingdownSharedRunnerCert (via the one-statement wrapper), and gwtc3_ringdown_shared_runner_one_statement, which packages runner presence, refactored-script count $3$, mapping count $2$, and this smoke equality into a single conjunction with a nonempty certificate.
In the Recognition verification stack this is bookkeeping, not physics: it locks the post-refactor smoke surface so the guarded-family runner cannot silently drop tests. It does not touch the forcing chain (T0–T8), RCL, mass ladder, or $\alpha$ band; it only certifies that the GWTC-3 ringdown script refactor still runs its smoke suite cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.