sample_member_is_h5
plain-language theorem explainer
The inspected GWTC-3 ringdown ZIP member is fixed as the path rin/rin_S190727h_pyring_DS_1mode_10M.h5. Anyone citing the one-member HDF5 schema certificate needs this identity. The proof is reflexivity against the named string constant.
Claim. The sample member name equals the string $\texttt{rin/rin\_S190727h\_pyring\_DS\_1mode\_10M.h5}$.
background
This module freezes a schema-level inspection of one real HDF5 posterior file from the GWTC-3 ringdown ZIP, obtained without fetching the full 1.44 GB archive. The method is: HTTP range-read of the ZIP central directory, selection of the smallest .h5 member, range-read of that member's local header and compressed payload, local inflate, then h5py schema walk.
The sample member name is the string constant recording that chosen path. Companion live metadata (compressed size 679110 bytes, uncompressed 931208, 97 HDF5 objects, posterior dataset /EXP6/posterior_samples with 15114 samples and 7 fields) sits in sibling constants. The module is structural only: schema facts, not posterior likelihood.
proof idea
One-line rfl. The left-hand side is the definitional constant equal to that exact string, so definitional equality closes the goal.
why it matters
Feeds the bundled certificate gwtc3RingdownHDF5SampleSchemaCert as the field sample_member_named, and appears as the first conjunct of gwtc3_ringdown_hdf5_sample_schema_one_statement. That one-statement theorem packages member identity, object-count split, posterior path, positive sample count, and field count into a single claim.
In the Verification domain this pins which physical file the schema numbers refer to, so downstream reproducibility scripts and certificates cannot silently drift to another ZIP member. It is not an RS forcing-chain step (T0–T8); it is empirical schema lock-in for GWTC-3 ringdown data used in later checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.