summary_member_matches_schema
plain-language theorem explainer
The GWTC-3 ringdown summary module hard-codes the same HDF5 member path as the sample schema: both name the file rin/rin_S190727h_pyring_DS_1mode_10M.h5. Anyone wiring the posterior-summary certificate to the schema cites this equality. The proof is pure definitional equality by rfl.
Claim. The summary module's recorded HDF5 member path equals the schema's sample member path: both are the string $\texttt{rin/rin\_S190727h\_pyring\_DS\_1mode\_10M.h5}$.
background
This module freezes the first posterior-summary statistics pulled from a range-read GWTC-3 ringdown HDF5 file (member rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, 15114 samples, seven fields). It is structural bookkeeping only: column names and basic ranges for a later likelihood parser, not an RS echo or QNM likelihood.
The companion schema module defines the canonical sample member name as the string literal for that same HDF5 path. The summary module repeats an identical string constant for its own member name. Aligning the two constants is the first field of the summary certificate record.
proof idea
One-line wrapper by rfl. Both sides reduce to the same string literal, so the equality is definitional and needs no lemmas or rewriting.
why it matters
Feeds the certificate constructor gwtc3RingdownHDF5SampleSummaryCert, which packages four schema-alignment facts (member, path, sample count, field count). Without this equality the certificate record cannot be inhabited. In the verification layer it locks the summary extract to the same GWTC-3 ringdown member the schema advertises, so downstream parsers cannot silently drift to a different file. It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it is data-contract hygiene for the GWTC-3 ringdown pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.