sampleRootAttrCount
plain-language theorem explainer
Records that the inspected GWTC-3 ringdown HDF5 sample has zero attributes on the root group. Citation target for schema-level reproducibility checks against the live ZIP member. The body is a literal natural-number constant, not a derived proof.
Claim. The root-group attribute count of the sampled GWTC-3 ringdown HDF5 member is $0$.
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 include compressed size 679110 bytes, uncompressed size 931208 bytes, 97 HDF5 objects (14 groups, 83 datasets), and the key posterior path /EXP6/posterior_samples with 15114 samples and 7 fields. Among those counts, the root group carries no attributes. This is structural bookkeeping only, not a posterior-likelihood claim.
proof idea
Definitional constant: the value is the literal natural number 0, matching the live h5py root-attribute count from the companion inspection script. No lemmas or tactics.
why it matters
Pins one concrete cell of the GWTC-3 ringdown sample schema inside the Verification domain so downstream reproducibility statements can quote an in-tree Nat rather than an external notebook. The module status is structural theorem (0 sorry, 0 RS-internal axiom). It does not touch the forcing chain (T0–T8), RCL, or mass-ladder physics; it only anchors observational data layout used by verification pipelines that may later compare ringdown posteriors to RS predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.