GuardDecision
plain-language theorem explainer
Two-valued decision type for the GWTC-3 ringdown runtime family guard: accept or reject. Downstream policy code cites it as the return type of the model-name classifier that admits only the three Session-131 mapped families. The declaration is a plain inductive with decidable equality; no proof content.
Claim. An inductive type with two constructors, accept and reject, equipped with decidable equality. It is the codomain of the GWTC-3 ringdown family guard that classifies model-family names as either admitted or blocked.
background
The module formalizes a runtime policy induced by the Session 131 family-stratified likelihood selector for GWTC-3 ringdown analyses. It does not compute posteriors; it only records which model-family strings the selector treats as eligible.
Eligible families are the three mapped ones: DS single-mode at 10M, Kerr 220 at 0M, and Kerr 220 at 10M. Everything else (Kerr 221 variants, MMRDNP, pseobnrv4hm, and unknown names) is blocked. The decision type is the discrete answer space for that policy check.
Status is structural: zero sorry and no new Recognition-Science axioms. The import chain pulls Mathlib and the upstream likelihood-selector module that defines the family stratification being guarded.
proof idea
Definitional inductive with two nullary constructors. Decidable equality is derived automatically by Lean; there is no tactic proof or lemma application.
why it matters
Supplies the return type for guardModel, the string classifier that accepts only DS_1mode_10M, Kerr_220_0M, and Kerr_220_10M and rejects all other names. Sibling lemmas then prove acceptance and rejection facts for each representative family, and count eligible versus blocked models.
In the Verification domain this is pure runtime-policy formalization: it pins the Session-131 family gate in Lean so downstream checks cannot silently widen the admitted set. It does not touch the forcing chain (T0–T8), the Recognition Composition Law, or mass/ladder physics; it only hardens the GWTC-3 ringdown model filter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.