smoke_after_refactor_all_passed
plain-language theorem explainer
All seven post-refactor smoke tests for the GWTC-3 ringdown shared guarded-family runner pass. Verification authors cite it when assembling the shared-runner certificate. The proof is reflexivity: both sides are the literal natural number 7.
Claim. The number of smoke tests that pass after the shared-runner refactor equals the total number of smoke tests after that refactor (both equal $7$).
background
This module is a structural verification layer for the GWTC-3 ringdown analysis. It records a refactor that moved controlled-family damping scripts onto one shared guarded runner. The runner enforces require_eligible_model(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)$ mapping).
The two constants compared here are pure Nat literals: smokeTestsAfterRefactor is defined as 7, and smokePassesAfterRefactor is also defined as 7. They encode an external smoke-suite tally after the refactor, not a derived physical quantity. The module states explicitly that this is a refactor/safety invariant only: no new physics mapping and no posterior likelihood computation.
proof idea
One-line term proof by rfl. Both sides reduce definitionally to the same Nat literal 7, so equality holds by reflexivity with no lemmas or tactics required.
why it matters
Feeds the master certificate gwtc3RingdownSharedRunnerCert as the smoke_passed field, and appears as one conjunct in the one-statement theorem gwtc3_ringdown_shared_runner_one_statement. That parent packages runner presence, refactored script count (3), supported mapping count (2), this smoke equality, and nonemptiness of the cert structure.
Within Recognition Science verification, the declaration closes a safety check on the GWTC-3 ringdown guarded-family path after consolidating four scripts onto the shared runner. It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it only certifies that the post-refactor smoke suite is fully green, supporting the module claim of structural closure with zero sorry and zero new RS-internal axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.