guard_all_tests_passed
plain-language theorem explainer
The master boolean for the GWTC-3 ringdown family-guard test suite equals true: every programmed accept/reject check succeeds. Verification authors cite it when packaging the runtime policy into a certificate or a single conjunction. The proof is reflexivity against a definition fixed to true.
Claim. The master flag asserting that all GWTC-3 ringdown family-guard unit tests pass is equal to $\mathrm{true}$.
background
This module formalizes a runtime policy for GWTC-3 ringdown model families induced by the Session 131 family-stratified likelihood selector. It is structural only: it records which named families the guard accepts or rejects, and computes no posterior likelihood. Status is closed (zero sorry, zero new RS-specific axioms).
The guard accepts exactly three mapped families: DS one-mode at $10M$, Kerr $220$ at $0M$, and Kerr $220$ at $10M$. It rejects blocked or unknown families, including Kerr $221$ at $0M$, Kerr $221$ with $\mathrm{d}\omega_{221}$ at $0M$, MMRDNP at $10M$, pseobnrv4hm, and any unrecognized name.
Upstream, guardAllTestsPassed is a Boolean definition fixed to true, standing for the conjunction of the individual accept/reject lemmas in the module.
proof idea
One-line term proof by rfl. The Boolean guardAllTestsPassed is defined as the constant true, so equality to true is definitional and closes immediately.
why it matters
This is the master-cert hinge for the GWTC-3 ringdown family guard. Downstream, gwtc3RingdownFamilyGuardCert packages the individual accept/reject lemmas into a single certificate record, and gwtc3_ringdown_family_guard_one_statement restates the full accept/reject conjunction as one theorem. Both depend on the suite having passed.
In the Recognition verification layer this is policy formalization, not a forcing-chain step (T0–T8) or a mass/ladder claim. It locks the Session 131 selector’s family stratification into machine-checked runtime guards so blocked models cannot silently enter ringdown analyses that claim RS-aligned selection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.