sampleDatasetCount
plain-language theorem explainer
Numeric constant fixing the dataset count of the inspected GWTC-3 ringdown HDF5 sample at 83. Schema-certificate and object-count lemmas cite it to pin the live metadata snapshot. The body is a bare Nat literal from the companion range-read inspection script.
Claim. The inspected GWTC-3 ringdown HDF5 sample member contains exactly $83$ datasets.
background
The module freezes a one-member schema snapshot 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 includes compressed size 679110, uncompressed size 931208, 97 HDF5 objects, 14 groups, 83 datasets, and the key posterior path /EXP6/posterior_samples with 15114 samples and 7 fields. Sibling constants record each of those figures as Lean Nat or String literals so downstream certificates can name them.
This is structural schema inspection only: object and dataset tallies, not posterior likelihood or RS mass/ladder physics.
proof idea
Definition, not a proved theorem. The body is the literal 83, matching the live h5py dataset count reported in the module doc. No tactics, no lemmas.
why it matters
Feeds three local consumers: the object-count split theorem (sampleGroupCount + sampleDatasetCount = sampleHDF5ObjectCount), the bundled schema certificate structure, and the one-statement schema theorem that conjoins member name, object split, posterior path, and field count.
In the Verification domain this is scaffolding for reproducible GWTC-3 ringdown checks against Recognition Science predictions. It does not itself touch the forcing chain (T0–T8), RCL, or the phi-ladder mass formula; it only locks the empirical HDF5 layout so later comparison lemmas have a fixed, sorry-free numerator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.