summaryFieldCount
plain-language theorem explainer
Records that the GWTC-3 ringdown HDF5 posterior sample has exactly seven columns. Verification authors cite it when wiring schema equality and positivity checks into the sample-summary certificate. The body is a one-line natural-number literal.
Claim. The posterior-sample field count for the range-read GWTC-3 ringdown HDF5 summary is the natural number $7$.
background
This module freezes the first posterior-summary statistics taken from a single GWTC-3 ringdown HDF5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples). The recorded sample has 15114 rows and seven named columns: $\psi$, $\log A_{t_0}$, $f_{t_0}$, $\tau_{t_0}$, $\phi_{t_0}$, $\log L$, and $\log\mathrm{Prior}$.
The constant sits beside sibling literals for member name, dataset path, sample count, and per-field means and quantiles. It is structural bookkeeping only: one-member posterior summary, not an RS echo or QNM likelihood. Companion extraction lives in papers/reproducibility/gwtc3_ringdown_hdf5_sample_summary.py. The module claims zero sorry and no new RS-specific axioms.
proof idea
Pure definition: the natural number is set to the literal $7$. No lemmas, tactics, or computation beyond the constant binding.
why it matters
Feeds four local consumers. The certificate structure GWTC3RingdownHDF5SampleSummaryCert requires field_count_matches_schema : summaryFieldCount = posteriorFieldCount. The matching theorem is a reflexivity proof against the schema constant. Positivity 0 < summaryFieldCount is discharged by unfold and decide. The one-statement summary theorem packages summaryFieldCount = 7 with sample-count and mean-sign facts so downstream parsers can rely on a fixed column arity.
In the broader Verification domain this locks the column layout needed by later likelihood parsers. It does not touch the forcing chain (T0–T8), RCL, or mass-ladder physics; it only certifies observational bookkeeping for GWTC-3 ringdown data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.