summary_field_count_matches_schema
plain-language theorem explainer
The GWTC-3 ringdown HDF5 posterior summary records exactly seven fields, matching the fixed schema field count. Reproducibility and verification authors cite this when assembling the sample-summary certificate. The proof is pure reflexivity: both sides reduce definitionally to the natural number 7.
Claim. The field count of the extracted GWTC-3 ringdown HDF5 posterior summary equals the schema field count: both equal $7$.
background
This module freezes the first posterior-summary statistics read from one GWTC-3 ringdown HDF5 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 posteriorFieldCount as the natural number 7 (the seven named posterior columns: psi, log amplitude, frequency, damping time, phase, log-likelihood, log-prior). The summary side defines summaryFieldCount the same way from the extracted file. Equality of those two constants is the local claim.
proof idea
One-line reflexivity. Both summaryFieldCount and posteriorFieldCount are defined as the literal natural number 7, so rfl closes the equality by definitional reduction. No lemmas or tactics beyond that.
why it matters
Feeds the bundled certificate gwtc3RingdownHDF5SampleSummaryCert, which packages member path, sample count, and field-count agreement as a single record. That certificate is the machine-checkable anchor that the Python extraction script and the Lean schema describe the same seven-column posterior table.
In the broader Verification lane this is infrastructure, not a physics derivation: it locks the column layout before any Recognition-Science mass ladder, eight-tick, or alpha-band claim is attached to ringdown data. Zero sorry and no new RS axioms; it only certifies that the summary and schema agree on field cardinality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.