smoke_pass_count_eq_test_count
plain-language theorem explainer
The GWTC-3 ringdown smoke suite reports seven passes out of seven tests: pass count equals test count by definition. Anyone assembling the guarded-family scripts certificate cites this equality. The proof is pure reflexivity on two Nat literals both equal to 7.
Claim. The number of smoke tests that pass equals the total number of smoke tests: both quantities equal $7$.
background
This module is Session 133 structural bookkeeping for GWTC-3 ringdown family scripts. Three mapped damping-family scripts (DS1 mode 10M, Kerr 220 0M, Kerr 220 10M) now call a runtime eligibility guard before reading posterior data. The guard is operational only: no new physics mapping and no new likelihood.
Two sibling Nat definitions fix the smoke-suite size: the total test count is 7, and the recorded pass count is also 7. The suite is meant to confirm that eligible families pass the guard while representative blocked or unknown families fail. This equality is the numeric half of that smoke claim.
proof idea
Term-mode reflexivity. Both sides reduce to the literal natural number 7, so rfl closes the goal with no lemmas and no rewriting beyond definitional unfolding.
why it matters
Feeds the certificate bundle gwtc3RingdownGuardedFamilyScriptsCert as the smoke_count field, alongside the boolean all-passed flag, the guarded-script count match, and the three per-family acceptance lemmas. Together those fields close the Session 133 claim that the runtime family guard is wired into the mapped scripts with a clean smoke suite. This is verification scaffolding for GWTC-3 ringdown analysis, not a step in the T0–T8 forcing chain or a new mass/alpha prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.