sample_posterior_dataset_named
plain-language theorem explainer
Records that the key posterior dataset inside the inspected GWTC-3 ringdown HDF5 member sits at the path /EXP6/posterior_samples. Schema-verification and GWTC-3 reproducibility work cite this as the named anchor for the 15,114-sample posterior table. The proof is pure reflexivity on the string constant that stores that path.
Claim. The recorded HDF5 path of the key posterior-samples dataset equals $\texttt{/EXP6/posterior\_samples}$.
background
This module freezes a one-member schema inspection of the GWTC-3 ringdown ZIP without fetching the full 1.44 GB archive. A companion script range-reads the ZIP central directory, picks the smallest .h5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5), inflates only that member, and inspects it with h5py.
Among the live metadata (97 HDF5 objects, 14 groups, 83 datasets, 15,114 posterior samples, 7 fields) the inspection identifies a single key posterior table. The string constant posteriorSamplesDatasetPath stores that table's absolute path inside the file. The present theorem simply pins that constant to the observed path string.
The setting is structural verification only: schema layout and counts, not posterior likelihood or full-catalog statistics.
proof idea
One-line term proof by rfl. The left-hand side is the definitional constant whose body is already the string "/EXP6/posterior_samples", so definitional equality closes the goal immediately.
why it matters
Feeds the master certificate gwtc3RingdownHDF5SampleSchemaCert and the bundled one-statement theorem gwtc3_ringdown_hdf5_sample_schema_one_statement, which conjoins member name, object-count split, this path equality, positive sample count, and field count equals 7. Together they close the STRUCTURAL THEOREM status of the module (0 sorry, 0 RS-internal axioms).
In the broader Recognition verification layer this is infrastructure, not a forcing-chain step: it locks the observed HDF5 layout so later claims about ringdown posteriors cannot silently drift to a different dataset path. No T0–T8 landmark is at stake; the value is reproducibility of the external GWTC-3 sample schema.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.