Verification Gwtc3 Ringdown Hdf5 Sample Summary

Data grounding for a physics pipeline

The GWTC-3 ringdown HDF5 sample summary is a small, precisely scoped record inside the Recognition Science framework's machine-checked library of formal theorems. It captures the first posterior-summary statistics extracted from a range-read GWTC-3 ringdown HDF5 file. The file is named rin/rin_S190727h_pyring_DS_1mode_10M.h5, and the dataset inside it is at the path /EXP6/posterior_samples. The record states that this dataset contains 15,114 samples across 7 fields: psi, logA_t_0, f_t_0, tau_t_0, phi_t_0, logL, and logPrior. These are the column names and basic numerical ranges needed by a later likelihood parser.

The purpose is deliberately narrow. It is a one-member posterior summary only, not an RS echo or quasinormal-mode likelihood. The record establishes the schema and sign facts that a downstream parser will rely on. It proves, for example, that the sample count is positive, that the field count is positive, that the mean of the log-prior is zero, and that the mean of the log-amplitude is negative. It also records the quantile order for the frequency and damping-time fields, showing that the 16th percentile is below the median, which is below the 84th percentile. These are structural facts about the data, not physical claims about gravitational waves.

In plain language, this is a receipt. It says: this specific data file has this many samples, these columns, and these basic statistical properties, all checked by the framework's kernel. The companion script that produced the summary is papers/reproducibility/gwtc3_ringdown_hdf5_sample_summary.py. The status is a structural theorem with zero sorry and zero RS-internal axioms, meaning the kernel checked every step. The master certificate, gwtc3RingdownHDF5SampleSummaryCert, bundles all these facts into a single inhabitant, and a one-statement theorem packages the whole summary for easy reference.

What this changes for a reader is the confidence that the data pipeline starts on solid ground. Before any physics can be derived from a gravitational-wave ringdown, the file format and its contents must be understood exactly. This record provides that grounding, and it does so with the same rigor as the framework's more abstract theorems. The numbers themselves, such as a mean frequency of 420.95 Hz and a median frequency of 345.41 Hz, are not predictions; they are measurements recorded from the file. The value is in the proof that these numbers are what the schema says they are.

/-- One-statement posterior-summary theorem for the range-read HDF5 sample. -/
theorem gwtc3_ringdown_hdf5_sample_summary_one_statement :
    (summarySampleCount = 15114) ∧
    (summaryFieldCount = 7) ∧
    (0 < fMean) ∧
    (0 < tauMean) ∧
    (logAMean < 0) ∧
    (logPriorMean = 0) ∧
    (fQ16 < fMedian ∧ fMedian < fQ84) ∧
    (tauQ16 < tauMedian ∧ tauMedian < tauQ84) ∧
    Nonempty GWTC3RingdownHDF5SampleSummaryCert :=
  ⟨rfl, rfl,
   mean_signs.2.2.1,
   mean_signs.2.2.2.1,
   mean_signs.2.1,
   mean_signs.2.2.2.2.2.2,
   f_quantile_order,
   tau_quantile_order,
   gwtc3RingdownHDF5SampleSummaryCert_inhabited⟩

theorem mean_signs :
    0 < psiMean ∧ logAMean < 0 ∧ 0 < fMean ∧ 0 < tauMean ∧
      0 < phiMean ∧ 0 < logLMean ∧ logPriorMean = 0 := by
  unfold psiMean logAMean fMean tauMean phiMean logLMean logPriorMean
  norm_num

theorem f_quantile_order :
    fQ16 < fMedian ∧ fMedian < fQ84 := by
  unfold fQ16 fMedian fQ84
  norm_num

theorem gwtc3RingdownHDF5SampleSummaryCert_inhabited :
    Nonempty GWTC3RingdownHDF5SampleSummaryCert :=
  ⟨gwtc3RingdownHDF5SampleSummaryCert⟩

What this page does not claim

This record does not derive any physical property of the gravitational-wave source. This record does not perform a likelihood calculation or an RS echo analysis. This record does not establish the correctness of the companion Python script, only the facts recorded from its output.

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