Verification Gwtc3 Ringdown Guarded Family Scripts

Guarded analysis scripts

Gravitational-wave astronomy extracts the properties of a ringing black hole from the decaying signal it emits after a merger. This ringdown signal is compared against theoretical models, each predicting a particular set of frequencies and damping times. The choice of model shapes the posterior distributions that researchers report, so an analysis that accidentally uses the wrong model produces numbers that look valid but are not.

The verification module named GWTC-3 Ringdown Guarded Family Scripts addresses this risk with a runtime guard. Three Python scripts, each analyzing a different ringdown model family, now call a function named require_eligible_model before they read any posterior data. This function checks that the model identifier passed to the script is on an approved list. The three approved identifiers are DS_1mode_10M, Kerr_220_0M, and Kerr_220_10M.

The module proves, in a machine-checked library of formal theorems, that these three scripts are guarded and that the guard behaves correctly. The proof establishes that all three approved models are accepted, and that three representative unapproved models, including Kerr_221_0M and pseobnrv4hm, are rejected. A smoke test with seven cases confirms the guard passes all seven. The entire certificate is a single formal object, and the library records zero unproved assumptions and zero framework-specific axioms.

This is operational guarding, not new physics. The module adds no new mapping between theory and data and computes no new likelihood. Its purpose is to prevent a silent error class: an analysis that runs with the wrong model and produces a confident but meaningless result. By making the guard a proved theorem, the framework turns a runtime check into a documented fact that future readers can audit.

def guardedScriptCount : Nat := 3

theorem representative_blocked_rejected :
    guardModel "Kerr_221_0M" = .reject ∧
    guardModel "MMRDNP_10M" = .reject ∧
    guardModel "pseobnrv4hm" = .reject :=
  ⟨guard_rejects_Kerr2210, guard_rejects_MMRDNP, guard_rejects_pseobnrv4hm⟩

theorem smoke_all_passed : smokeAllPassed = true := rfl

/-- One-statement theorem for the guarded family scripts. -/
theorem gwtc3_ringdown_guarded_family_scripts_one_statement :
    (guardedScriptCount = 3) ∧
    (smokeTestCount = 7) ∧
    (smokePassCount = 7) ∧
    (smokeAllPassed = true) ∧
    (guardModel "DS_1mode_10M" = .accept) ∧
    (guardModel "Kerr_220_0M" = .accept) ∧
    (guardModel "Kerr_220_10M" = .accept) ∧
    Nonempty GWTC3RingdownGuardedFamilyScriptsCert :=
  ⟨rfl, rfl, rfl, rfl,
   guard_accepts_DS,
   guard_accepts_Kerr2200,
   guard_accepts_Kerr22010,
   gwtc3RingdownGuardedFamilyScriptsCert_inhabited⟩

What this page does not claim

This module does not derive or verify any new gravitational-wave physics. The guard does not validate the scientific quality of the approved models themselves. The module does not prove that the three approved models are the correct ones for any real event.

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/GWTC3RingdownGuardedFamilyScripts.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: