Verification Gwtc3 Ringdown Family Comparison

The ringdown family comparison

When two black holes merge, the new black hole rings like a struck bell, emitting gravitational waves that decay in a characteristic pattern called the ringdown. The GWTC-3 catalog, the third gravitational-wave transient catalog from the LIGO-Virgo-KAGRA collaboration, contains observed ringdown signals. This comparison examines how well three different theoretical models, or families, describe that data.

The three families are named by their assumptions. The first, DS_1mode_10M, is a single damped sinusoid model with a ten-solar-mass reference. The other two are based on the Kerr solution of general relativity, which describes a rotating black hole, using the dominant 2-2 mode: one with zero initial spin (Kerr_220_0M) and one with a spin of ten (Kerr_220_10M). The comparison uses a pooled set of 66 members and 1,954,998 samples from the catalog.

The verified result is a strict ordering of the three families by their pooled means and medians. The DS model has the highest mean and median, followed by Kerr_220_0M, and then Kerr_220_10M. The differences are positive and explicit: 0.143 between DS and Kerr_220_0M, and 0.089 between Kerr_220_0M and Kerr_220_10M. This means that, on average, the DS model assigns higher probability to the observed data than either Kerr model.

The ordering also holds for how often each model's predictions fall within the observed data's confidence intervals. The DS model's predictions are inside the pooled 68% and 90% intervals. Kerr_220_0M falls inside the 90% interval only. Kerr_220_10M falls inside neither. These inclusion facts are proven as a chain of inequalities on the counts of members inside the intervals.

In Recognition Science, this is a verification module, meaning it checks a prediction against measured data. The framework models the cost of recognition, and its forcing chain derives physical constants and scaling laws. Here, the framework's prediction is that the DS model, which aligns with its derived structure, should fit the ringdown data better than the Kerr alternatives. The comparison confirms this ordering is not a coincidence of a single sample but holds across the pooled set.

The comparison is deliberately narrow. It is a three-family comparison, not a mixed-model archive-wide likelihood. It does not claim that DS is the best possible model, only that it beats these two Kerr models on this data. The result is a structural theorem: it proves the ordering facts from the data and the model definitions, with zero unproved assumptions in the framework's machine-checked library of formal theorems.

theorem family_mean_order :
    kerr22010PooledMean < kerr2200PooledMean ∧
      kerr2200PooledMean < dsPooledMean := by
  exact ⟨kerr22010_mean_lt_kerr2200_mean, ds_vs_kerr_mean_order⟩

theorem hit_count_order :
    kerr22010MembersInside68Count < kerr2200MembersInside68Count ∧
      kerr2200MembersInside68Count < dsMembersInside68Count := by
  unfold kerr22010MembersInside68Count kerr2200MembersInside68Count dsMembersInside68Count
  decide

theorem comparison_total_members :
    dsFamilyMemberCount + kerr2200MemberCount + kerr22010MemberCount =
      comparisonTotalMembers := by
  unfold dsFamilyMemberCount kerr2200MemberCount kerr22010MemberCount comparisonTotalMembers
  decide

theorem comparison_total_samples :
    dsFamilyTotalSampleCount + kerr2200TotalSampleCount + kerr22010TotalSampleCount =
      comparisonTotalSamples := by
  unfold dsFamilyTotalSampleCount kerr2200TotalSampleCount kerr22010TotalSampleCount
    comparisonTotalSamples
  decide

What this page does not claim

This module does not prove that the DS model is the best possible ringdown model. This module does not provide a physical derivation of the DS model from the framework's forcing chain. This module does not claim that the Kerr model is wrong, only that it fits this data less well.

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