sample_sizes_pos
plain-language theorem explainer
Both the compressed and uncompressed byte sizes of the inspected GWTC-3 ringdown HDF5 sample are strictly positive. Authors of the sample-schema certificate cite this as the positivity half of the size checks. The proof unfolds the two fixed natural-number constants and finishes by decidable comparison.
Claim. For the selected GWTC-3 ringdown HDF5 sample member, the compressed size $679110$ and the uncompressed size $931208$ both satisfy $0 < n$.
background
This module freezes a one-member schema inspection of the GWTC-3 ringdown ZIP: the smallest .h5 posterior member is range-read from the central directory, inflated locally, and summarized with h5py, without pulling the full 1.44 GB archive. Live metadata include compressed size $679110$ bytes and uncompressed size $931208$ bytes, plus offsets, object/group/dataset counts, and the key posterior path /EXP6/posterior_samples.
The two constants used here are exactly those recorded sizes: compressed size is the natural $679110$, uncompressed size is $931208$. The claim is only that both are positive naturals, a minimal well-formedness guard before comparing them or packing the certificate structure. The module is marked structural theorem status: zero sorry, zero new RS-internal axioms.
proof idea
Term/tactic hybrid: unfold the two size definitions to the concrete naturals $679110$ and $931208$, then run decide on the conjunction of strict inequalities against zero. No lemmas beyond definitional unfolding; positivity is pure closed arithmetic on fixed Nat literals.
why it matters
Feeds the sizes_positive field of the sample-schema certificate bundle, which also requires the member name to be an .h5, uncompressed size strictly above compressed size, and the object-count split into groups plus datasets. That certificate is the Lean-side closure of the companion reproducibility script's live metadata pass.
In the Recognition verification layer this is infrastructure, not a forcing-chain step: it pins that the inspected posterior member is a non-empty compressed payload with a non-empty inflated body, so later schema facts (object counts, posterior sample and field counts) sit on a non-vacuous file. It does not touch J-cost, phi-ladder masses, or T0–T8; it only hardens the GWTC-3 ringdown data handle used by external checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.