Verification Gwtc3 Ringdown Family Guard

The family guard

Gravitational-wave astronomy often fits a detected signal to a family of theoretical models. Each family describes a different physical assumption about the source, such as the black hole's spin or the number of quasinormal modes in the ringdown. The verification module called GWTC-3 Ringdown Family Guard is a small, machine-checked gatekeeper: it formally records which model families a particular analysis pipeline is allowed to use.

The guard is a simple function. It takes a model family's name as a string and returns either accept or reject. It accepts exactly three families: DS_1mode_10M, Kerr_220_0M, and Kerr_220_10M. It rejects every other input, including representative blocked families such as Kerr_221_0M, MMRDNP_10M, pseobnrv4hm, and any unknown name. The guard proves, as formal theorems, that each of these eight test cases produces the intended decision.

This is runtime-policy formalization only. The guard computes no posterior likelihood and performs no physics. It does not judge whether one model fits the data better than another. Its job is narrower: to enforce a pre-existing selection of allowed families, so that a pipeline cannot silently run a model outside the approved list. The guard's own documentation states this explicitly, and the proofs are axiom-clean, with zero sorry and zero new Recognition Science-specific axioms.

The guard also records the counts from the runtime test: three eligible models, eleven blocked models, eight test cases total, three accepted and five rejected, and a boolean flag guardAllTestsPassed set to true. Two theorems tie these counts back to the selector's own lists, and a third proves the accepted and rejected counts sum to the total. A master certificate structure packages the whole result, and a final one-statement theorem bundles the acceptance, rejection, and certificate existence into a single conjunction.

In plain language, the guard is a formal promise. It says: given these eight named inputs, the pipeline will accept exactly the three intended families and reject the five others, and this behavior is machine-verified rather than merely asserted. The value is not in the decision logic itself, which is a trivial string comparison, but in the fact that the decision is locked into a machine-checked library of formal theorems, so a future change to the selector cannot silently break the guard without failing the proof.

theorem guard_accepts_DS :
    guardModel "DS_1mode_10M" = .accept := by
  unfold guardModel
  simp

theorem guard_accepts_Kerr2200 :
    guardModel "Kerr_220_0M" = .accept := by
  unfold guardModel
  simp

theorem guard_accepts_Kerr22010 :
    guardModel "Kerr_220_10M" = .accept := by
  unfold guardModel
  simp

theorem guard_rejects_Kerr2210 :
    guardModel "Kerr_221_0M" = .reject := by
  unfold guardModel
  simp

theorem guard_rejects_MMRDNP :
    guardModel "MMRDNP_10M" = .reject := by
  unfold guardModel
  simp

theorem guard_rejects_pseobnrv4hm :
    guardModel "pseobnrv4hm" = .reject := by
  unfold guardModel
  simp

theorem guard_rejects_unknown :
    guardModel "not_a_real_family" = .reject := by
  unfold guardModel
  simp

/-- One-statement runtime guard theorem. -/
theorem gwtc3_ringdown_family_guard_one_statement :
    (guardModel "DS_1mode_10M" = .accept) ∧
    (guardModel "Kerr_220_0M" = .accept) ∧
    (guardModel "Kerr_220_10M" = .accept) ∧
    (guardModel "Kerr_221_0M" = .reject) ∧
    (guardModel "MMRDNP_10M" = .reject) ∧
    (guardModel "pseobnrv4hm" = .reject) ∧
    (guardAllTestsPassed = true) ∧
    Nonempty GWTC3RingdownFamilyGuardCert :=
  ⟨guard_accepts_DS,
   guard_accepts_Kerr2200,
   guard_accepts_Kerr22010,
   guard_rejects_Kerr2210,
   guard_rejects_MMRDNP,
   guard_rejects_pseobnrv4hm,
   guard_all_tests_passed,
   gwtc3RingdownFamilyGuardCert_inhabited⟩

What this page does not claim

The guard does not compute any posterior likelihood or perform any physics. The guard does not prove that the accepted models are physically correct. The guard does not claim to cover every possible model family name.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/GWTC3RingdownFamilyGuard.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: