sampleGroupCount
plain-language theorem explainer
Records that the inspected GWTC-3 ringdown HDF5 sample contains exactly 14 groups. Verification authors cite it when locking the live schema snapshot into Lean. It is a bare natural-number constant taken from the companion range-read inspection, not a derived proof.
Claim. The number of HDF5 groups in the inspected sample member is $14$.
background
The module freezes a one-member schema snapshot of the GWTC-3 ringdown posterior archive without pulling the full 1.44 GB ZIP. 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, uncompressed size 931208, HDF5 object count 97, group count 14, dataset count 83, and root attribute count 0. Sibling constants pin the other fields; this definition holds only the group count.
The setting is structural verification only: schema shape of one posterior file, not likelihoods or RS mass/ladder physics.
proof idea
No proof body. The declaration is a definitional constant Nat := 14, transcribed from the live h5py group count reported in the module documentation. Downstream lemmas unfold it and discharge equalities by decide.
why it matters
Feeds three local consumers. sample_object_count_split unfolds this constant with the dataset and object counts to prove groups plus datasets equal total HDF5 objects. GWTC3RingdownHDF5SampleSchemaCert packages it into the schema certificate structure. gwtc3_ringdown_hdf5_sample_schema_one_statement includes the same split in the single conjunction that freezes the sample schema.
In the broader Verification domain this is empirical lock-in of external LIGO/Virgo ringdown data layout, not a step of the T0–T8 forcing chain. It closes the structural half of the GWTC-3 ringdown reproducibility path (status: 0 sorry, 0 RS-internal axioms).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.