sampleUncompressedSize
plain-language theorem explainer
The uncompressed byte length of the smallest GWTC-3 ringdown HDF5 posterior member is fixed at 931208. Verification authors cite this constant when certifying the one-member schema inspection against live ZIP metadata. The declaration is a bare natural-number literal with no proof obligations.
Claim. The inspected GWTC-3 ringdown HDF5 sample member has uncompressed size $931208$ bytes.
background
The 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 (rin/rin_S190727h_pyring_DS_1mode_10M.h5), range-reads its local header and compressed bytes, inflates locally, and inspects the schema with h5py.
Live metadata from that inspection includes compressed size 679110 bytes, uncompressed size 931208 bytes, local-header and data offsets, object/group/dataset counts, and the key posterior path /EXP6/posterior_samples with 15114 samples and 7 fields. Sibling constants pin the other measured quantities; this definition holds only the uncompressed length.
The setting is structural verification only: one-member schema inspection, not posterior likelihood, with zero sorry and no new RS-specific axioms.
proof idea
Definition by literal. The body is the natural number 931208, matching the live inflated size reported by the companion reproducibility script. No tactics, lemmas, or proof terms are involved.
why it matters
This constant is one of the measured schema anchors for the GWTC-3 ringdown sample certificate. It is required by GWTC3RingdownHDF5SampleSchemaCert (via the positivity and uncompressed-greater-than-compressed fields), by the theorem that both compressed and uncompressed sizes are positive, and by the theorem that uncompressed size strictly exceeds compressed size.
Those facts close the structural side of the one-member HDF5 inspection: the archive member is non-empty after inflation and exhibits genuine compression. The module status is a structural theorem (closure 2026-05-22) supporting reproducibility of GWTC-3 ringdown data layout inside the Recognition verification layer. It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it is pure observational schema pinning.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.