summary_sample_count_matches_schema
plain-language theorem explainer
The GWTC-3 ringdown HDF5 posterior summary records the same sample count as the schema constant: both equal 15114. Verification authors cite this when wiring the sample-summary certificate. The proof is pure reflexivity on matching natural-number literals.
Claim. The recorded summary sample count equals the schema posterior sample count; both are the natural number $15114$.
background
This module freezes the first posterior-summary statistics taken from a range-read GWTC-3 ringdown HDF5 file (member rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples). It is structural bookkeeping only: column names and basic counts for a later likelihood parser, not an RS echo or QNM fit.
The schema side fixes posteriorSamplesCount := 15114. The summary side fixes the parallel constant summarySampleCount := 15114. Equality of those two Nats is the local claim. Companion extraction lives in papers/reproducibility/gwtc3_ringdown_hdf5_sample_summary.py.
proof idea
One-line reflexivity: both sides reduce to the same Nat literal 15114, so rfl closes the goal with no lemmas or rewriting.
why it matters
Feeds the certificate record gwtc3RingdownHDF5SampleSummaryCert as the field sample_count_matches_schema. That cert bundles member path, sample count, and field count matches so downstream verification can treat the HDF5 summary as schema-aligned. It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it only locks observational bookkeeping needed before any ringdown likelihood is stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.