posteriorSamplesDatasetPath
plain-language theorem explainer
Canonical string naming the key posterior dataset inside the inspected GWTC-3 ringdown HDF5 member: `/EXP6/posterior_samples`. Schema certs and the one-statement sample theorem cite it to pin the live h5py path. Defined by literal equality; no proof obligations.
Claim. The HDF5 path of the posterior-samples dataset in the inspected GWTC-3 ringdown member is the string $/\mathrm{EXP6}/\mathrm{posterior\_samples}$.
background
The module records a structural, one-member schema inspection of an actual HDF5 posterior file from the GWTC-3 ringdown ZIP, obtained without downloading the full 1.44 GB archive. A companion script range-reads the ZIP central directory, selects the smallest .h5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5), inflates only that member, and inspects it with h5py.
Live metadata include 97 HDF5 objects (14 groups, 83 datasets), zero root attributes, and a distinguished posterior dataset at path /EXP6/posterior_samples holding 15,114 samples across 7 fields. Sibling constants fix member name, compressed/uncompressed sizes, offsets, and those counts. This is schema geometry only, not a likelihood or mass-ladder claim.
proof idea
Pure definition: the identifier is bound to the string literal "/EXP6/posterior_samples". Downstream equalities discharge by rfl against this constant. No lemmas, tactics, or hypotheses.
why it matters
Anchors the schema certificate GWTC3RingdownHDF5SampleSchemaCert and the bundled theorem gwtc3_ringdown_hdf5_sample_schema_one_statement, which conjoins member name, object-count additivity, this path, positive sample count, and field count 7. The thin wrapper sample_posterior_dataset_named is exactly rfl at this definition. The summary layer reuses it: summary_path_matches_schema and GWTC3RingdownHDF5SampleSummaryCert.path_matches_schema require the summary posterior path to equal this string, so schema and summary stay synchronized. In the Verification domain this is empirical bookkeeping for GWTC-3 ringdown posteriors, not a step of the T0–T8 forcing chain; it closes the structural claim that the inspected member really exposes the expected posterior dataset path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.