summaryPosteriorPath
plain-language theorem explainer
Fixes the HDF5 internal path string for the GWTC-3 ringdown posterior samples dataset as "/EXP6/posterior_samples". Verification authors cite it when locking the one-member sample summary against the schema. The body is a literal string constant, not a derived computation.
Claim. The recorded path of the posterior-samples dataset inside the GWTC-3 ringdown HDF5 member is the string $/\mathrm{EXP6}/\mathrm{posterior\_samples}$.
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). The purpose is structural only: pin column names, sample count (15114), field count (7), and basic numerical ranges so a later likelihood parser has a fixed schema. It is not an RS echo or QNM likelihood.
The companion schema module supplies the expected dataset path name posteriorSamplesDatasetPath. The present definition is the observed path extracted by the reproducibility script gwtc3_ringdown_hdf5_sample_summary.py. Matching the two strings is the content of the path-consistency certificate field.
proof idea
Pure definition: a String constant equal to "/EXP6/posterior_samples". No tactics, no lemmas. Downstream equality proofs discharge by rfl against the schema path.
why it matters
Feeds the certificate structure GWTC3RingdownHDF5SampleSummaryCert, whose field path_matches_schema requires summaryPosteriorPath = posteriorSamplesDatasetPath, and the one-line theorem summary_path_matches_schema that proves that equality by reflexivity. Together they close the structural layer of the GWTC-3 ringdown HDF5 sample summary (status: structural theorem, 0 sorry, 0 new RS axioms). The path lock is a prerequisite for any later parser that reads the seven posterior fields (psi, logA_t_0, f_t_0, tau_t_0, phi_t_0, logL, logPrior). It does not itself touch the forcing chain, RCL, or mass ladder; it is verification scaffolding for observational data ingest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.