summary_path_matches_schema
plain-language theorem explainer
The summary module's posterior dataset path equals the schema path string "/EXP6/posterior_samples". Anyone assembling the GWTC-3 ringdown HDF5 sample-summary certificate cites this equality. The proof is pure reflexivity: both sides are the same string literal.
Claim. The recorded summary posterior path equals the schema posterior-samples dataset path: both are the string $/\mathrm{EXP6}/\mathrm{posterior\_samples}$.
background
This module freezes the first posterior-summary statistics pulled from one GWTC-3 ringdown HDF5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5). It is structural bookkeeping only: column names, sample count, and basic numerical ranges for a later likelihood parser, not an RS echo or QNM fit.
The schema module defines the canonical dataset path as the string "/EXP6/posterior_samples". The summary module repeats that same literal under its own name. Matching the two strings is one of the four field equalities required by the sample-summary certificate structure.
proof idea
One-line reflexivity. Both summaryPosteriorPath and posteriorSamplesDatasetPath reduce to the identical string literal "/EXP6/posterior_samples", so rfl closes the goal with no lemmas.
why it matters
Feeds the path_matches_schema field of gwtc3RingdownHDF5SampleSummaryCert, the bundled certificate that the extracted summary agrees with the schema on member name, path, sample count, and field count. Without this equality the certificate record cannot be inhabited. The module is marked structural closure (zero sorry, zero new RS axioms); it only pins I/O conventions needed before any RS physics claim about ringdown posteriors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.