sample_posterior_samples_nonempty
plain-language theorem explainer
The inspected GWTC-3 ringdown HDF5 member has a strictly positive posterior sample count (15,114 draws). Schema and reproducibility auditors cite this when packaging the one-member HDF5 inspection into a single certificate. The proof unfolds the concrete Nat constant and closes by decidable comparison.
Claim. The recorded posterior sample count for the inspected GWTC-3 ringdown HDF5 member is strictly positive: $0 < 15114$.
background
This module freezes a schema-level inspection of one real HDF5 posterior member from the GWTC-3 ringdown ZIP, obtained by HTTP range reads of the ZIP central directory and the smallest .h5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5), then local inflate and h5py inspection. It is structural metadata only, not a likelihood or full-catalog claim.
Among the frozen constants is the length of the key posterior dataset /EXP6/posterior_samples. That length is the Nat definition posteriorSamplesCount := 15114, matching the live metadata result (15,114 samples, 7 fields). Positivity of that count is the minimal non-degeneracy check before the sample can enter a certificate bundle.
proof idea
Term-style proof: unfold the definition of the posterior sample count to the concrete natural 15114, then decide discharges $0 < 15114$ by the decidable order on Nat. No lemmas beyond definitional unfolding.
why it matters
Feeds the bundled certificate gwtc3RingdownHDF5SampleSchemaCert and the conjunction theorem gwtc3_ringdown_hdf5_sample_schema_one_statement, which packages member name, object-count split, posterior path, sample positivity, and field count into one statement. In the Recognition verification layer this is empirical scaffolding closure: a zero-sorry record that the ringdown posterior member actually carries a nonempty sample table, so downstream GW checks are not vacuous on empty data. It does not touch the forcing chain (T0–T8) or RCL; it anchors observational schema facts used by reproducibility scripts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.