IndisputableMonolith.Verification.GWTC3RingdownFamilyGuard
Runtime acceptance guard for GWTC-3 ringdown model families: which templates may enter family-stratified likelihood scripts and which are blocked. Downstream guarded-family scripts import it so only eligible models (DS, Kerr2200, Kerr22010) pass. Structure is a decision type plus one-line accept/reject lemmas and two count tallies.
claimA runtime guard on GWTC-3 ringdown families decides accept or reject for each named model. Eligible: DS, Kerr $2200$, Kerr $22010$. Blocked: Kerr $2210$, Kerr $221\Delta\omega$, MMRDNP, pSEOBNRv4HM, and unknown. The module exposes the decision type, the model classifier, accept/reject lemmas for each case, and counts of eligible versus blocked models.
background
This sits in the Verification domain of the Recognition Science monolith. Upstream, the GWTC-3 ringdown likelihood selector records the structural policy for future family-stratified ringdown likelihoods (status: structural theorem, zero sorry, closed 2026-05-22). That selector maps which waveform families are eligible for likelihood work.
The present module turns that policy into a one-statement runtime guard. Sibling names show a decision type (GuardDecision), a classifier on model tags, explicit accept lemmas for DS and two Kerr variants, reject lemmas for several Kerr and phenomenological templates plus unknown, and two tallies of eligible versus blocked models.
Local setting: ringdown post-merger templates used against GWTC-3 data must be filtered before family-statistic scripts run, so only the mapped eligible set participates.
proof idea
Definition-plus-lemma module, not a single deep proof. It introduces a decision type and a model classifier, then proves one-line accept or reject facts by case on each named family tag (DS and two Kerr modes accepted; Kerr 2210, Kerr 221 with frequency shift, MMRDNP, pSEOBNRv4HM, and unknown rejected). Two counting lemmas report how many models fall on each side of the guard. No heavy tactic machinery; the argument is exhaustive case analysis against the upstream selector policy.
why it matters in Recognition Science
Feeds GWTC3RingdownGuardedFamilyScripts, which records Session 133: the runtime family guard is wired into the mapped family-statistic scripts. Without this gate, stratified ringdown likelihoods could silently include blocked templates. In the Verification layer it closes the policy-to-runtime path for GWTC-3 ringdown family selection (structural, zero sorry). It does not itself derive masses, coupling constants, or forcing-chain steps (T0–T8); it is an observational-analysis hygiene theorem that keeps only the selector-eligible families in the scripted statistics.
scope and limits
- Does not derive or fit ringdown waveforms to GWTC-3 strain data.
- Does not prove physical correctness of DS or Kerr templates.
- Does not compute numerical likelihood values or posterior odds.
- Does not extend the eligible set beyond the upstream selector policy.
- Does not address non-ringdown GWTC-3 analyses or other catalogs.
used by (1)
depends on (1)
declarations in this module (23)
-
inductive
GuardDecision -
def
guardModel -
theorem
guard_accepts_DS -
theorem
guard_accepts_Kerr2200 -
theorem
guard_accepts_Kerr22010 -
theorem
guard_rejects_Kerr2210 -
theorem
guard_rejects_Kerr221Domega -
theorem
guard_rejects_MMRDNP -
theorem
guard_rejects_pseobnrv4hm -
theorem
guard_rejects_unknown -
def
guardEligibleModelCount -
def
guardBlockedModelCount -
def
guardTestCount -
def
guardAcceptedTestCount -
def
guardRejectedTestCount -
def
guardAllTestsPassed -
theorem
guard_counts_match_selector -
theorem
guard_test_count_partition -
theorem
guard_all_tests_passed -
structure
GWTC3RingdownFamilyGuardCert -
def
gwtc3RingdownFamilyGuardCert -
theorem
gwtc3RingdownFamilyGuardCert_inhabited -
theorem
gwtc3_ringdown_family_guard_one_statement