summarySampleCount
plain-language theorem explainer
Fixes the GWTC-3 ringdown posterior sample size at 15114 for the range-read HDF5 member rin/rin_S190727h_pyring_DS_1mode_10M.h5. Verification and schema-matching lemmas cite this constant so sample-count equalities and positivity are definitional. The body is a bare Nat literal; no proof work.
Claim. The posterior sample count extracted from the GWTC-3 ringdown HDF5 dataset is the natural number $15114$.
background
This module freezes the first posterior-summary statistics from a single GWTC-3 ringdown HDF5 file (member rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples). The extraction is structural only: column names and basic numerical ranges for a later likelihood parser, not an RS echo or QNM likelihood.
Companion schema constants (member name, posterior path, field count, and the seven fields psi, logA_t_0, f_t_0, tau_t_0, phi_t_0, logL, logPrior) live in the imported sample-schema module. The sample count is recorded here as a named Nat so downstream certificates can equate it to the schema value by reflexivity and prove positivity by decide.
Status is structural theorem: zero sorry, zero new RS-specific axioms.
proof idea
Definitional constant: the body is the literal natural number 15114. No tactics, no lemmas. Downstream equalities such as summarySampleCount = posteriorSamplesCount are rfl; positivity unfolds the definition and closes by decide.
why it matters
Pins the sample size that the certificate structure GWTC3RingdownHDF5SampleSummaryCert requires via sample_count_matches_schema and sample_count_pos. The one-statement theorem gwtc3_ringdown_hdf5_sample_summary_one_statement opens with the equality summarySampleCount = 15114, and the matching lemmas summary_sample_count_matches_schema and summary_sample_count_pos discharge the corresponding certificate fields.
In the broader Verification domain this is infrastructure for reproducible GWTC-3 ringdown ingestion, not a Recognition Science forcing-chain step (T0–T8) or mass-ladder claim. It closes the sample-count half of the structural summary so later parsers can trust the column layout and N without re-reading the HDF5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.