sampleCompressedSize
plain-language theorem explainer
Records the compressed byte length of the smallest GWTC-3 ringdown HDF5 member inspected by range request: 679110. Verification authors cite it when locking the live ZIP schema into Lean. It is a bare Nat literal, not a derived proof.
Claim. The compressed size of the sample HDF5 member $\texttt{rin/rin\_S190727h\_pyring\_DS\_1mode\_10M.h5}$ is the natural number $679110$ (bytes).
background
The module freezes a one-member schema inspection of the GWTC-3 ringdown ZIP without pulling the full 1.44 GB archive. Method: HTTP range-read of the ZIP central directory, select the smallest .h5 member, range-read its local header and compressed payload, inflate locally, and inspect with h5py.
Live metadata from that pass includes compressed size 679110 bytes, uncompressed size 931208 bytes, local-header offset 66237197, and data offset 66237294, plus HDF5 object/group/dataset counts. Companion constants in the same file pin the member name, offsets, and posterior dataset path /EXP6/posterior_samples.
This is structural bookkeeping only: schema facts about one ZIP member, not a likelihood or mass-ladder claim.
proof idea
No proof. The declaration is a definition equal to the literal natural number 679110, matching the compressed-size field reported by the companion reproducibility script.
why it matters
Feeds three local consumers: the positivity theorem sample_sizes_pos (both sizes strictly positive), the comparison sample_uncompressed_gt_compressed (compressed strictly less than uncompressed), and the certificate structure GWTC3RingdownHDF5SampleSchemaCert, whose sizes_positive and uncompressed_gt_compressed fields package those facts.
In the Recognition verification layer this is infrastructure, not a forcing-chain step (T0–T8). It closes the structural theorem status of the module (0 sorry, 0 new RS axioms) by pinning the live compressed length so downstream Lean checks cannot drift from the measured ZIP member.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.