IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSchema

   1import Mathlib
   2import IndisputableMonolith.Verification.GWTC3RingdownZipSchema
   3
   4/-!
   5# GWTC-3 Ringdown HDF5 Sample Schema
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9This module records the first schema-level inspection of an actual HDF5
  10posterior member from the GWTC-3 ringdown ZIP, without downloading the
  11full 1.44 GB archive.
  12
  13Companion script:
  14
  15* `papers/reproducibility/gwtc3_ringdown_hdf5_sample_schema.py`
  16
  17Method:
  18
  19* Read ZIP central directory by HTTP range request.
  20* Select the smallest `.h5` member:
  21  `rin/rin_S190727h_pyring_DS_1mode_10M.h5`.
  22* Range-read that member's local header and compressed bytes only.
  23* Inflate locally and inspect the HDF5 schema with `h5py`.
  24
  25Live metadata result:
  26
  27* compressed size: `679,110` bytes
  28* uncompressed size: `931,208` bytes
  29* local-header offset: `66,237,197`
  30* data offset: `66,237,294`
  31* HDF5 object count: `97`
  32* group count: `14`
  33* dataset count: `83`
  34* root attr count: `0`
  35* key posterior dataset: `/EXP6/posterior_samples`
  36* posterior sample count: `15,114`
  37* posterior field count: `7`
  38
  39This is one-member schema inspection only, not posterior likelihood.
  40Zero `sorry`. Zero new RS-specific axioms.
  41-/
  42
  43namespace IndisputableMonolith
  44namespace Verification
  45namespace GWTC3RingdownHDF5SampleSchema
  46
  47open IndisputableMonolith.Verification.GWTC3RingdownZipSchema
  48
  49/-! ## §1. Sample member constants -/
  50
  51def sampleMemberName : String := "rin/rin_S190727h_pyring_DS_1mode_10M.h5"
  52def sampleCompressedSize : Nat := 679110
  53def sampleUncompressedSize : Nat := 931208
  54def sampleLocalHeaderOffset : Nat := 66237197
  55def sampleDataOffset : Nat := 66237294
  56def sampleHDF5ObjectCount : Nat := 97
  57def sampleGroupCount : Nat := 14
  58def sampleDatasetCount : Nat := 83
  59def sampleRootAttrCount : Nat := 0
  60def posteriorSamplesDatasetPath : String := "/EXP6/posterior_samples"
  61def posteriorSamplesCount : Nat := 15114
  62def posteriorFieldCount : Nat := 7
  63
  64/-! ## §2. Schema facts -/
  65
  66theorem sample_sizes_pos :
  67    0 < sampleCompressedSize ∧ 0 < sampleUncompressedSize := by
  68  unfold sampleCompressedSize sampleUncompressedSize
  69  decide
  70
  71theorem sample_uncompressed_gt_compressed :
  72    sampleCompressedSize < sampleUncompressedSize := by
  73  unfold sampleCompressedSize sampleUncompressedSize
  74  decide
  75
  76theorem sample_object_count_split :
  77    sampleGroupCount + sampleDatasetCount = sampleHDF5ObjectCount := by
  78  unfold sampleGroupCount sampleDatasetCount sampleHDF5ObjectCount
  79  decide
  80
  81theorem sample_posterior_samples_nonempty :
  82    0 < posteriorSamplesCount := by
  83  unfold posteriorSamplesCount
  84  decide
  85
  86theorem sample_posterior_field_count_pos :
  87    0 < posteriorFieldCount := by
  88  unfold posteriorFieldCount
  89  decide
  90
  91theorem sample_member_is_h5 :
  92    sampleMemberName = "rin/rin_S190727h_pyring_DS_1mode_10M.h5" := rfl
  93
  94theorem sample_posterior_dataset_named :
  95    posteriorSamplesDatasetPath = "/EXP6/posterior_samples" := rfl
  96
  97/-! ## §3. Master cert -/
  98
  99structure GWTC3RingdownHDF5SampleSchemaCert where
 100  sample_member_named :
 101    sampleMemberName = "rin/rin_S190727h_pyring_DS_1mode_10M.h5"
 102  sizes_positive :
 103    0 < sampleCompressedSize ∧ 0 < sampleUncompressedSize
 104  uncompressed_gt_compressed :
 105    sampleCompressedSize < sampleUncompressedSize
 106  object_count_split :
 107    sampleGroupCount + sampleDatasetCount = sampleHDF5ObjectCount
 108  posterior_dataset_named :
 109    posteriorSamplesDatasetPath = "/EXP6/posterior_samples"
 110  posterior_samples_nonempty :
 111    0 < posteriorSamplesCount
 112  posterior_field_count_pos :
 113    0 < posteriorFieldCount
 114  ringdown_zip_schema_available :
 115    Nonempty GWTC3RingdownZipSchemaCert
 116
 117def gwtc3RingdownHDF5SampleSchemaCert :
 118    GWTC3RingdownHDF5SampleSchemaCert where
 119  sample_member_named := sample_member_is_h5
 120  sizes_positive := sample_sizes_pos
 121  uncompressed_gt_compressed := sample_uncompressed_gt_compressed
 122  object_count_split := sample_object_count_split
 123  posterior_dataset_named := sample_posterior_dataset_named
 124  posterior_samples_nonempty := sample_posterior_samples_nonempty
 125  posterior_field_count_pos := sample_posterior_field_count_pos
 126  ringdown_zip_schema_available := gwtc3RingdownZipSchemaCert_inhabited
 127
 128theorem gwtc3RingdownHDF5SampleSchemaCert_inhabited :
 129    Nonempty GWTC3RingdownHDF5SampleSchemaCert :=
 130  ⟨gwtc3RingdownHDF5SampleSchemaCert⟩
 131
 132/-- One-statement HDF5 sample schema theorem. -/
 133theorem gwtc3_ringdown_hdf5_sample_schema_one_statement :
 134    (sampleMemberName = "rin/rin_S190727h_pyring_DS_1mode_10M.h5") ∧
 135    (sampleGroupCount + sampleDatasetCount = sampleHDF5ObjectCount) ∧
 136    (posteriorSamplesDatasetPath = "/EXP6/posterior_samples") ∧
 137    (0 < posteriorSamplesCount) ∧
 138    (posteriorFieldCount = 7) ∧
 139    Nonempty GWTC3RingdownHDF5SampleSchemaCert :=
 140  ⟨sample_member_is_h5,
 141   sample_object_count_split,
 142   sample_posterior_dataset_named,
 143   sample_posterior_samples_nonempty,
 144   rfl,
 145   gwtc3RingdownHDF5SampleSchemaCert_inhabited⟩
 146
 147end GWTC3RingdownHDF5SampleSchema
 148end Verification
 149end IndisputableMonolith
 150