GWTC3RingdownFamilyGuardCert
plain-language theorem explainer
Certificate bundle for the GWTC-3 ringdown runtime family guard: three mapped families are accepted, blocked and unknown families are rejected, and the guard counts match the Session 131 likelihood selector. Verification and GWTC-3 pipeline authors cite it as the single Prop packing those policy facts. As a structure it has no proof body; inhabitants are built by discharging each field with the corresponding guard lemmas.
Claim. A certificate is a record asserting: the guard accepts $\mathrm{DS\_1mode\_10M}$, $\mathrm{Kerr\_220\_0M}$, and $\mathrm{Kerr\_220\_10M}$; rejects $\mathrm{Kerr\_221\_0M}$, $\mathrm{MMRDNP\_10M}$, $\mathrm{pseobnrv4hm}$, and any unknown family string; eligible and blocked model counts equal the selector's ($3$ and $11$); accepted plus rejected test counts equal the total test count; all guard tests pass; and the likelihood-selector certificate type is inhabited.
background
This module formalizes the runtime policy induced by the Session 131 family-stratified likelihood selector for GWTC-3 ringdown analyses. It is structural only: it records which model-family strings the guard admits, and computes no posterior likelihood. Status is closed (zero sorry, zero new RS-internal axioms).
The decision function maps a model name to accept or reject. Exactly three strings are accepted: the single-mode DS family at $10M$, and the Kerr $(2,2,0)$ family at $0M$ and $10M$. Every other string, including representative blocked families (Kerr $(2,2,1)$, MMRDNP, pseobNR, unknowns), is rejected. Companion Nat/Bool constants fix eligible count $3$, blocked count $11$, accepted tests $3$, rejected tests $5$, total tests, and the all-passed flag.
The certificate also requires that those counts agree with the upstream selector's eligible/blocked tallies and that a nonempty selector certificate exists, tying the runtime guard to the likelihood-selector layer.
proof idea
No proof body: this is a structure whose fields are propositions (equalities of guard decisions, Nat/Bool identities, and Nonempty of the selector cert). An inhabitant is assembled by filling each field with a named lemma such as the accept facts for DS and the two Kerr220 variants, the reject facts for Kerr221, MMRDNP, pseobNR, and unknown strings, plus the count and partition equalities and the selector Nonempty witness. Downstream, the canonical instance wires those lemmas fieldwise; inhabitedness is then a one-constructor wrap of that instance.
why it matters
This structure is the typed contract for the GWTC-3 ringdown family guard. The canonical certificate value, the Nonempty theorem, and the one-statement conjunction theorem are all built on it, so any consumer that needs a single object asserting accept/reject policy plus count integrity depends here. Downstream, the guarded-family scripts certificate reuses the eligible-model count and smoke-pass flags against this same guard surface.
In the Recognition verification stack this is runtime-policy formalization for GWTC-3 ringdown model families, not a derivation from the forcing chain (T0–T8) or the Recognition Composition Law. It closes the Session 131 selector-induced guard as a checkable Lean record: only the three mapped families may pass, blocked and unknown families are excluded, and selector tallies are mirrored. That keeps later scripts and audits from silently widening the admitted model set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.