Verification Gwtc3 Ringdown Kerr2200 Mdamping Family

A family of ringdown tests

Gravitational-wave astronomy records the final stage of a black-hole merger as a ringdown: the newly formed black hole vibrates like a struck bell, emitting a decaying tone. The decay rate, called the damping, carries information about the hole's mass and spin. The quality factor Q, a standard measure of how many oscillations occur before the tone fades, is used to convert a spin value into a damping-per-cycle number. For a black hole with spin parameter a, the standard Berti-style Kerr-220 fit gives Q_220(a) = 0.7000 + 1.4187 (1-a)^(-0.4990), and the damping per cycle is exp(-π / Q_220).

The Recognition Science framework, which derives physical constants from a single cost function, predicts a specific value for this damping-per-cycle: the inverse of the golden ratio, 1/φ ≈ 0.618. The question is whether this prediction appears in real data. The framework's machine-checked library of formal theorems, a collection of verified mathematical statements, records the comparison. It takes 22 events from the GWTC-3 catalog, all modeled as Kerr black holes with the 220 mode, and pools 647,220 posterior samples of the damping statistic.

The result is a structural theorem, not a claim of discovery. The pooled mean damping is 0.4382, with a 90% interval from 0.2493 to 0.6439. The predicted target 0.618 falls inside this 90% interval, but outside the tighter 68% interval. Only 3 of the 22 individual events have their own 68% intervals containing the target. The framework proves these interval facts as formal theorems, with zero unproved assumptions. The one-statement theorem packages the whole comparison: the counts, the interval containments, and the fact that the Kerr-family mean is lower than the mean from a different (damped-sinusoid) model family.

What this establishes in plain language is a controlled, honest test. The framework's predicted damping value is not ruled out by the pooled data, but it is also not strongly confirmed. The target sits in the broad middle of the distribution, not at its center. The module does not claim a detection or a precise match. It records a structural fact: the golden-ratio prediction is compatible with the observed spread of ringdown dampings, at the 90% level, across a specific family of 22 events. This is a step in a larger verification program, one that treats the framework's constants as testable predictions against astronomical data.

def kerr2200PooledMean : ℝ := 0.438208510863

def kerr2200PooledQ05 : ℝ := 0.249303771620

def kerr2200PooledQ95 : ℝ := 0.643869947920

theorem kerr2200_target_inside_pooled_90 :
    kerr2200PooledQ05 < kerr2200RSDampingTarget ∧
      kerr2200RSDampingTarget < kerr2200PooledQ95 := by
  obtain ⟨hlo, hhi⟩ := Constants.PhiLadder.phi_inv_bracket_tight
  unfold kerr2200PooledQ05 kerr2200RSDampingTarget kerr2200PooledQ95
  constructor <;> linarith

theorem kerr2200_target_not_inside_pooled_68 :
    kerr2200PooledQ84 < kerr2200RSDampingTarget := by
  obtain ⟨hlo, _hhi⟩ := Constants.PhiLadder.phi_inv_bracket_tight
  unfold kerr2200PooledQ84 kerr2200RSDampingTarget
  linarith

def kerr2200MembersInside68Count : Nat := 3

/-- One-statement Kerr-family damping theorem. -/
theorem gwtc3_ringdown_kerr2200m_damping_family_one_statement :
    (kerr2200MemberCount = 22) ∧
    (kerr2200EventCount = 22) ∧
    (kerr2200TotalSampleCount = 647220) ∧
    (kerr2200PooledQ05 < kerr2200RSDampingTarget ∧
      kerr2200RSDampingTarget < kerr2200PooledQ95) ∧
    (kerr2200PooledQ84 < kerr2200RSDampingTarget) ∧
    (kerr2200PooledMean < dsPooledMean) ∧
    Nonempty GWTC3RingdownKerr2200MDampingFamilyCert :=
  ⟨rfl, rfl, rfl,
   kerr2200_target_inside_pooled_90,
   kerr2200_target_not_inside_pooled_68,
   ds_vs_kerr_mean_order,
   gwtc3RingdownKerr2200MDampingFamilyCert_inhabited⟩

What this page does not claim

The target is not claimed to be the center of the distribution, only inside the 90% interval. This does not claim a detection of the golden-ratio value in gravitational-wave data. The module does not address whether the 22 events are a complete or unbiased sample of ringdowns.

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