smokeAllPassed
plain-language theorem explainer
Hardcodes the aggregate smoke-test flag for GWTC-3 ringdown guarded family scripts as true. Verification authors cite it when packaging the Session 133 guard wiring into a certificate or one-statement theorem. The body is a one-line Boolean constant, not a derived computation.
Claim. The aggregate smoke-test outcome for the guarded GWTC-3 ringdown family scripts is the Boolean value $\mathrm{true}$.
background
Session 133 wires a 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 an eligibility check before reading posterior data. The module records only operational guarding: no new physics mapping and no new likelihood.
Sibling counters track how many scripts are guarded, how many smoke tests run, and how many pass. The present flag is the Boolean summary that all smoke checks succeeded (eligible families accepted; representative blocked or unknown families rejected). Downstream certificates and the one-statement theorem assert equality of this flag with true.
proof idea
Definitional constant: the Boolean is set to true by construction. No lemmas, tactics, or computation. The companion theorem smoke_all_passed discharges smokeAllPassed = true by reflexivity (rfl).
why it matters
Feeds the certificate structure GWTC3RingdownGuardedFamilyScriptsCert (field smoke_passed) and the bundled theorem gwtc3_ringdown_guarded_family_scripts_one_statement, which conjoins guard counts, smoke counts, this flag, and per-model accept/reject outcomes. It closes the Session 133 structural record that the runtime guard is live in the three patched scripts. Framework role is verification hygiene only: it does not touch the forcing chain (T0–T8), RCL, mass ladder, or alpha band. Zero sorry and no new RS axioms, matching the module status line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.