Verification Gwtc3 Ringdown One Member Rsstatistic

A single gravitational-wave check

Gravitational-wave astronomy records the final vibrations of a black hole as it settles after a merger, a signal called the ringdown. The posterior distribution of a ringdown amplitude parameter summarizes what the data allow. One such parameter, the logarithm of the amplitude of the dominant mode, comes from the event GWTC-3 S190727h, stored in the file rin/rin_S190727h_pyring_DS_1mode_10M.h5.

Recognition Science (RS) predicts a specific value for this logarithmic amplitude: log(φ^-44) ≈ -21.1733, where φ is the golden ratio. The framework's library, a machine-checked collection of formal theorems, records this as a structural target. The measured posterior mean from the data is -22.2446, with a standard deviation of about 0.398. The target lies about 2.69 standard deviations above the mean.

The library proves the target falls outside both the central 90% and 68% posterior intervals. The sample fraction of posterior draws above the target is only 0.000331. These are formal theorems, checked by the kernel with zero sorry and zero RS-specific axioms. They establish that this single measurement does not support the RS prediction for this amplitude parameter.

In plain language: one specific gravitational-wave event's data, when analyzed for the ringdown amplitude, do not match the value that Recognition Science expected. The mismatch is about 2.7 standard deviations, a clear tension for this one comparison. This is not a general verdict on RS; it is a single, precisely scoped statistical check.

def logAZFromMean : ℝ := 2.689626

theorem target_outside_90_interval :
    ¬ (logAQ05 ≤ rsLogPhiNeg44Target ∧ rsLogPhiNeg44Target ≤ logAQ95) := by
  intro h
  have hlt := target_above_q95
  linarith

theorem target_outside_68_interval :
    ¬ (logAQ16 ≤ rsLogPhiNeg44Target ∧ rsLogPhiNeg44Target ≤ logAQ84) := by
  intro h
  unfold logAQ84 rsLogPhiNeg44Target at h
  norm_num at h

def logAFractionAboveTarget : ℝ := 0.000331

/-- One-statement theorem for the one-member RS amplitude-scale statistic. -/
theorem gwtc3_ringdown_one_member_rs_statistic_one_statement :
    (logAQ95 < rsLogPhiNeg44Target) ∧
    (2 < logAZFromMean) ∧
    (logAFractionAboveTarget < 0.001) ∧
    Nonempty GWTC3RingdownOneMemberRSStatisticCert :=
  ⟨target_above_q95,
   z_from_mean_gt_two,
   fraction_above_target_small,
   gwtc3RingdownOneMemberRSStatisticCert_inhabited⟩

What this page does not claim

This does not claim that the RS prediction is wrong for all gravitational-wave events. This does not claim that the measured parameter is the final RS echo amplitude observable. This does not claim to have computed an archive-wide likelihood across all events.

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