Verification Gwtc3 Ringdown One Member Damping Statistic

A first damping comparison

When two black holes merge, the new black hole rings like a struck bell, emitting gravitational waves that fade in a characteristic way. The rate of that fading is called damping. In the GWTC-3 catalog of gravitational-wave events, one member, S190727h, has been measured and analyzed. The module verification gwtc3 ringdown one member damping statistic takes that one event's measured frequency and damping time, combines them into a single per-cycle damping ratio, and compares that ratio against a target derived within Recognition Science.

The comparison uses the measured quantities f_t_0 and tau_t_0, the ringdown frequency and damping time. Their product, f_t_0 times tau_t_0, gives the number of cycles in a damping time. The per-cycle damping ratio is exp(-1 / (f_t_0 * tau_t_0)), the fraction by which the oscillation's amplitude shrinks each cycle. For this one event, the median of that derived statistic is about 0.846, with a central 68% interval from about 0.553 to 0.950, and a central 90% interval from about 0.279 to 0.970.

The Recognition Science target for this damping ratio is the reciprocal of the golden ratio, phi^-1, approximately 0.618. This is not a decimal that resembles the target; it is the exact constant. The machine-checked library of formal theorems proves that phi^-1 lies inside both the 68% and the 90% intervals for this one event. The same library proves the statistic's z-score from the mean is below 1, meaning the target sits within one standard deviation of the measured distribution.

This is a single-member comparison, not an archive-wide claim. It does not establish that single-mode ringdown damping equals the final Recognition Science echo-train damping observable. What it does establish is a first physical mapping: a real gravitational-wave measurement, reduced to a per-cycle damping ratio, is consistent with the framework's predicted value. The module records this as a structural theorem with zero unproved assumptions, and it provides a certificate bundling the interval and z-score facts into one checkable statement.

def dampingMean : ℝ := 0.764591716607

/-- The RS damping target is the reciprocal golden ratio, not a decimal resembling it.

It used to be written `0.618033988750`, which made the interval theorems below
claims about a number someone typed. They are now claims about φ⁻¹ itself, which is
what the module always said it meant and what makes the comparison evidence.
`Verification.RingdownDampingTargetDerivation` proves this still reproduces the
published decimal to `2e-13`. -/
noncomputable def rsDampingTarget : ℝ := Constants.phi⁻¹

theorem damping_target_inside_68_interval :
    dampingQ16 < rsDampingTarget ∧ rsDampingTarget < dampingQ84 := by
  obtain ⟨hlo, hhi⟩ := Constants.PhiLadder.phi_inv_bracket_tight
  unfold dampingQ16 rsDampingTarget dampingQ84
  constructor <;> linarith

theorem damping_target_inside_90_interval :
    dampingQ05 < rsDampingTarget ∧ rsDampingTarget < dampingQ95 := by
  obtain ⟨hlo, hhi⟩ := Constants.PhiLadder.phi_inv_bracket_tight
  unfold dampingQ05 rsDampingTarget dampingQ95
  constructor <;> linarith

theorem damping_z_from_mean_lt_one :
    dampingZFromMean < 1 := by
  unfold dampingZFromMean
  norm_num

What this page does not claim

This module does not establish that single-mode ringdown damping equals the final Recognition Science echo-train damping observable. This is not an archive-wide comparison; it covers only the single member S190727h. The agreement does not prove the Recognition Science framework is correct; it is one consistency check against one 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/GWTC3RingdownOneMemberDampingStatistic.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: