sampleHDF5ObjectCount
plain-language theorem explainer
Records that the inspected GWTC-3 ringdown HDF5 sample contains exactly 97 objects (groups plus datasets). Verification authors cite it when locking the live schema snapshot into Lean. It is a bare natural-number constant, not a derived proof.
Claim. The inspected GWTC-3 ringdown HDF5 sample member has object count $97$.
background
The module freezes a one-member schema inspection of the GWTC-3 ringdown ZIP without pulling the full 1.44 GB archive. A companion script range-reads the ZIP central directory, selects the smallest .h5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5), inflates only that member, and inspects it with h5py.
Live metadata from that pass include compressed size 679110 bytes, uncompressed size 931208 bytes, 14 groups, 83 datasets, and therefore 97 HDF5 objects. Sibling constants pin the other counts and the key posterior path /EXP6/posterior_samples. This is structural bookkeeping only: schema shape, not posterior likelihood or RS mass formulae.
proof idea
No proof. The declaration is a definition that assigns the natural number 97, matching the live h5py object count from the companion inspection script. Downstream lemmas unfold this constant and discharge equalities by decide.
why it matters
Pins the object-count field of the frozen sample schema so Lean certificates cannot drift from the measured HDF5 layout. It is consumed by sample_object_count_split (groups plus datasets equal object count), by the aggregate certificate structure GWTC3RingdownHDF5SampleSchemaCert, and by the one-statement schema theorem that packages member name, object split, posterior path, sample count, and field count. In the Verification domain this is empirical scaffolding closure: zero sorry, zero new RS axioms, one concrete archive member. It does not touch the forcing chain (T0–T8), RCL, or phi-ladder mass formulae; it only anchors external GW data shape for later comparison work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.