posteriorSamplesCount
plain-language theorem explainer
Records the live count of rows in the key posterior dataset of the smallest GWTC-3 ringdown HDF5 member as the natural number 15114. Verification and reproducibility authors cite it when locking schema facts into certificates. The body is a bare constant definition, not a derived proof.
Claim. The inspected GWTC-3 ringdown HDF5 posterior dataset contains exactly $15114$ samples.
background
This 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.
Among the live metadata, the key posterior dataset is /EXP6/posterior_samples. The present definition stores its row count. Sibling constants record compressed/uncompressed sizes, object/group/dataset counts, the dataset path, and the field count (seven). The setting is structural verification only: schema shape, not posterior likelihood or RS dynamics.
proof idea
Pure definition: the natural-number constant is set to 15114. No tactics, lemmas, or computation beyond the literal assignment. Downstream non-emptiness proofs simply unfold this name and decide.
why it matters
Pins the sample-count field of the schema certificate and the one-statement schema theorem, both of which require 0 < posteriorSamplesCount together with path and field-count facts. The summary module equates its own summarySampleCount to this constant by reflexivity, so summary and schema stay synchronized.
In the broader Recognition verification layer this is empirical lock-in for GWTC-3 ringdown data layout, not a step of the T0–T8 forcing chain. It closes a reproducibility obligation: any later claim about this member’s posterior table size must match 15114 or the certificate fails.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.