Verification Gwtc3 Ringdown Likelihood Selector

Selector policy

The GWTC-3 ringdown likelihood selector is a policy, not a calculation. It is a rulebook that sorts the data files and model families from the third Gravitational-Wave Transient Catalog (GWTC-3) into two groups: those that are eligible for a ringdown likelihood analysis, and those that are blocked. The rulebook is written as a machine-checked library of formal theorems, meaning every count and every classification in it is verified by a computer proof assistant.

The policy draws a sharp line. Of the 243 HDF5 files in the catalog, exactly 66 are eligible and 177 are blocked. Of the 14 model families, exactly 3 are eligible and 11 are blocked. The three eligible families are DS_1mode_10M, which maps a direct damping signal; Kerr_220_0M and Kerr_220_10M, which map the quality factor of a black hole's 220 ringdown mode at two different starting times. Every family named Kerr_221* is blocked until a 221-mode mapping is formalized, as is every MMRDNP* family and the pseobnrv4hm waveform family.

The selector also enforces a rule against mixed aggregation: it never combines an eligible likelihood with a blocked one. The counts are not just asserted; they are proved to add up. The theorems selector_file_count_partition and selector_model_count_partition verify that the eligible and blocked counts sum exactly to the totals. A master certificate bundles these facts together, and a final theorem states the whole policy in one sentence: the totals are 243, 66, 177, 14, 3, 11, no mixed aggregation, and the certificate exists.

What this establishes in plain language is a discipline of honesty. The selector does not compute a posterior likelihood, and it does not claim that any model is correct. It only says which models are allowed to be considered, and it says so with machine-checked certainty. The blocked families are not rejected because they are wrong; they are blocked because their mapping to observable data has not yet been formalized. The selector is a gate that keeps the analysis honest until the missing formalizations arrive.

theorem selector_file_count_partition :
    selectorEligibleFiles + selectorBlockedFiles = selectorTotalHDF5Files := by
  unfold selectorEligibleFiles selectorBlockedFiles selectorTotalHDF5Files
  decide

theorem selector_model_count_partition :
    selectorEligibleModels + selectorBlockedModels = selectorTotalModels := by
  unfold selectorEligibleModels selectorBlockedModels selectorTotalModels
  decide

theorem selector_no_mixed_aggregation_true :
    selectorNoMixedAggregation = true := rfl

theorem gwtc3RingdownLikelihoodSelectorCert_inhabited :
    Nonempty GWTC3RingdownLikelihoodSelectorCert :=
  ⟨gwtc3RingdownLikelihoodSelectorCert⟩

def selectorNoMixedAggregation : Bool := true

What this page does not claim

The selector does not prove that any eligible model is physically correct. The selector does not compute a posterior likelihood or any measurement result. The blocked families are not rejected for being wrong, only for lacking a formalized mapping.

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