posteriorFieldCount
plain-language theorem explainer
Fixes the GWTC-3 ringdown HDF5 sample's posterior field count at seven, matching the live h5py inspection of `/EXP6/posterior_samples` in the smallest ZIP member. Citation target for schema certificates and the one-statement sample-schema theorem. The body is a bare natural-number constant, not a derived proof.
Claim. The inspected GWTC-3 ringdown HDF5 posterior samples table has exactly $7$ fields (columns).
background
The module freezes a one-member schema snapshot of the GWTC-3 ringdown posterior archive without pulling the full 1.44 GB ZIP. A companion Python script range-reads the ZIP central directory, picks the smallest .h5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5), inflates only that member, and inspects it with h5py.
Among the recorded live metadata are object/group/dataset counts and the key posterior path /EXP6/posterior_samples, which holds 15,114 samples. The field count of that dataset is the constant defined here. The module is structural verification only: schema shape, not likelihood or RS mass/forcing content.
proof idea
Definitional constant: the natural number seven, written as a def with no proof obligations. Downstream positivity is discharged by unfold plus decide; equality with summary-side counts is rfl.
why it matters
Pins the column dimension of the inspected posterior table so schema certificates can assert a concrete shape. It appears in GWTC3RingdownHDF5SampleSchemaCert, in the conjunct posteriorFieldCount = 7 of the one-statement schema theorem, and in the positivity lemma 0 < posteriorFieldCount. The summary module reuses it via summaryFieldCount = posteriorFieldCount and the matching field of GWTC3RingdownHDF5SampleSummaryCert, so summary and schema stay locked. This is archive-reproducibility scaffolding for GW ringdown data, not a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.