module module high

`IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSummary`

Records a one-statement posterior summary of a single range-read GWTC-3 ringdown HDF5 member: sample and field counts, path metadata, and means (plus a frequency quantile) for the stored columns. Gravitational-wave and Recognition verification work cites it as the frozen numeric snapshot between the schema layer and the one-member physical statistics. The module is structural bookkeeping over the already-inspected sample table, not a new inference engine.

claimFor one range-read GWTC-3 ringdown HDF5 posterior member, the module fixes the member name, posterior path, sample count $N$, field count, and the column means $\overline{\psi}$, $\overline{\log A}$, $\overline{f}$, $\overline{\tau}$, $\overline{\phi}$, $\overline{\log\mathcal{L}}$, $\overline{\log\pi}$, together with a frequency quantile $f_{Q16}$.

background

GWTC-3 is the LIGO–Virgo–KAGRA gravitational-wave transient catalog. Ringdown analyses fit quasinormal-mode (QNM) parameters on the post-merger waveform; the corresponding posterior tables are shipped as large HDF5 archives. The upstream schema module performs a structural, range-read inspection of one actual member without pulling the full ~1.44 GB ZIP, and declares that inspection closed (0 sorry, 0 RS-internal axiom).

This summary module sits directly on that schema. It freezes the member identity, path, $N$, field count, and the first-moment (and one quantile) statistics of the columns that later physical maps need: phase-like $\psi$, log-amplitude, frequency $f$, damping time $\tau$, an auxiliary phase $\phi$, and the likelihood/prior logs. No new sampling is performed; the numbers are the certified readout of the already-opened table.

proof idea

Definition and constant module, not a multi-step proof development. It names the summary fields (member, path, counts, means, $f_{Q16}$) as Lean values tied to the upstream HDF5 sample schema, so downstream modules can cite a single frozen posterior snapshot rather than re-opening the file layout. Argument structure is structural recording plus whatever one-statement theorem packages those constants; there is no analytic derivation inside the module.

why it matters in Recognition Science

Bridges raw schema inspection to the first physically interpreted one-member GWTC-3 ringdown checks in the Recognition verification stack. Downstream, the damping-statistic module maps $f_{t_0}$ and $\tau_{t_0}$ into a per-cycle QNM damping ratio; the RS-statistic module builds the first explicitly Recognition-referenced amplitude statistic on the same range-read table. Both import this summary so their claims rest on one shared, closed numeric member rather than ad hoc file reads. In the broader framework this is catalog verification infrastructure, not a forcing-chain (T0–T8) step; it anchors empirical ringdown numbers that later RS comparisons can cite without re-litigating HDF5 layout.

scope and limits

Does not download or certify the full 1.44 GB GWTC-3 ringdown archive.
Does not claim multi-event or catalog-wide posterior coverage; one member only.
Does not derive QNM damping ratios or RS amplitude maps (those live downstream).
Does not perform Bayesian re-inference; it records means and a quantile from an existing table.
Does not assert agreement with Recognition mass or alpha predictions by itself.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Verification.GWTC3RingdownOneMemberDampingStatistic module_import
IndisputableMonolith.Verification.GWTC3RingdownOneMemberRSStatistic module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSchema module_import

declarations in this module (30)

def summaryMemberName L37
def summaryPosteriorPath L38
def summarySampleCount L39
def summaryFieldCount L40
def psiMean L42
def logAMean L43
def fMean L44
def tauMean L45
def phiMean L46
def logLMean L47
def logPriorMean L48
def fQ16 L50
def fMedian L51
def fQ84 L52
def tauQ16 L54
def tauMedian L55
def tauQ84 L56
theorem summary_member_matches_schema L60
theorem summary_path_matches_schema L63
theorem summary_sample_count_matches_schema L66
theorem summary_field_count_matches_schema L69
theorem summary_sample_count_pos L72
theorem summary_field_count_pos L76
theorem mean_signs L80
theorem f_quantile_order L86
theorem tau_quantile_order L91
structure GWTC3RingdownHDF5SampleSummaryCert L98
def gwtc3RingdownHDF5SampleSummaryCert L112
theorem gwtc3RingdownHDF5SampleSummaryCert_inhabited L125
theorem gwtc3_ringdown_hdf5_sample_summary_one_statement L130