GWTC3RingdownHDF5SampleSchemaCert
plain-language theorem explainer
Certificate structure that packages schema-level invariants for one GWTC-3 ringdown HDF5 posterior member (the smallest .h5 in the archive). Verification and reproducibility work cites it as the typed bundle of member name, size inequalities, object-count split, and posterior path/count facts. It is a pure structure definition; a separate inhabitant plugs in the measured constants and the ZIP-schema nonempty witness.
Claim. A certificate record asserting: the sample member name equals $\mathrm{rin/rin\_S190727h\_pyring\_DS\_1mode\_10M.h5}$; compressed and uncompressed sizes are positive with compressed size strictly less than uncompressed; group count plus dataset count equals total HDF5 object count; the posterior-samples dataset path is $\texttt{/EXP6/posterior\_samples}$ with positive sample count and positive field count; and the companion GWTC-3 ringdown ZIP schema certificate is inhabited.
background
This module records a schema-level inspection of one actual HDF5 posterior member from the GWTC-3 ringdown ZIP, obtained without downloading the full 1.44 GB archive. The method reads the ZIP central directory by HTTP range request, selects the smallest .h5 member, range-reads only its local header and compressed bytes, inflates locally, and inspects the layout with h5py.
Live constants fixed in the module include compressed size $679{,}110$, uncompressed size $931{,}208$, $14$ groups, $83$ datasets ($97$ HDF5 objects), posterior path /EXP6/posterior_samples, $15{,}114$ posterior samples, and $7$ posterior fields. The structure also requires that the upstream ZIP-schema certificate type is inhabited, tying the member-level facts to the archive-level schema already recorded in GWTC3RingdownZipSchema.
Status is structural: zero sorry, zero new RS-internal axioms. This is one-member schema inspection only, not a posterior likelihood claim.
proof idea
No proof body: the declaration is a structure (record type) whose fields are propositions about named numeric and string constants. Inhabitance is discharged downstream by gwtc3RingdownHDF5SampleSchemaCert, which fills each field with a corresponding lemma (sample_member_is_h5, sample_sizes_pos, sample_uncompressed_gt_compressed, sample_object_count_split, and the analogous posterior and ZIP-schema facts). The structure itself only states the interface.
why it matters
Gives the typed surface for the first closed HDF5 sample-schema certificate in the GWTC-3 ringdown verification stack. Downstream, gwtc3RingdownHDF5SampleSchemaCert builds an inhabitant; gwtc3RingdownHDF5SampleSchemaCert_inhabited packages Nonempty of that type; and gwtc3_ringdown_hdf5_sample_schema_one_statement flattens the main equalities and positivity facts into a single conjunction.
GWTC3RingdownHDF5SampleSummaryCert then aligns a summary layer to this schema (member name, posterior path, sample count, field count). In the broader Recognition verification domain this is empirical scaffolding for gravitational-wave ringdown data hygiene, not a step of the T0–T8 forcing chain; it anchors reproducibility claims about real LIGO/Virgo posterior products that any later RS mass or timing comparison would need to trust.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.