IndisputableMonolith.Verification.GWTC3RingdownZipSchema

   1import Mathlib
   2import IndisputableMonolith.Verification.GWTC3PosteriorManifest
   3
   4/-!
   5# GWTC-3 Ringdown ZIP Schema
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9This module records the ZIP central-directory schema of
  10`IGWN-GWTC3-TGR-v1-rin.zip`, fetched by HTTP range request (central
  11directory only, no 1.44 GB payload download).
  12
  13Companion script:
  14
  15* `papers/reproducibility/gwtc3_ringdown_zip_schema.py`
  16
  17Live metadata result:
  18
  19* source ZIP size: `1,444,203,951` bytes
  20* central-directory offset: `1,444,176,371`
  21* central-directory size: `27,558` bytes
  22* entry count: `244`
  23* extension counts: `.h5 = 243`, `<none> = 1`
  24* top-level prefix: `rin = 244`
  25* total compressed size from entries: `1,444,151,741` bytes
  26* total uncompressed size from entries: `1,963,931,876` bytes
  27
  28This is schema inspection only, not posterior likelihood.
  29Zero `sorry`. Zero new RS-specific axioms.
  30-/
  31
  32namespace IndisputableMonolith
  33namespace Verification
  34namespace GWTC3RingdownZipSchema
  35
  36open IndisputableMonolith.Verification.GWTC3PosteriorManifest
  37
  38/-! ## §1. Schema constants -/
  39
  40def ringdownZipSourceSizeBytes : Nat := 1444203951
  41def ringdownZipCentralDirectoryOffset : Nat := 1444176371
  42def ringdownZipCentralDirectorySize : Nat := 27558
  43def ringdownZipEntryCount : Nat := 244
  44def ringdownZipH5Count : Nat := 243
  45def ringdownZipDirectoryMarkerCount : Nat := 1
  46def ringdownZipTopLevelRinCount : Nat := 244
  47def ringdownZipTotalCompressedSize : Nat := 1444151741
  48def ringdownZipTotalUncompressedSize : Nat := 1963931876
  49
  50/-! ## §2. Positivity and count facts -/
  51
  52theorem ringdown_zip_source_size_pos : 0 < ringdownZipSourceSizeBytes := by
  53  unfold ringdownZipSourceSizeBytes
  54  decide
  55
  56theorem ringdown_zip_cd_size_pos : 0 < ringdownZipCentralDirectorySize := by
  57  unfold ringdownZipCentralDirectorySize
  58  decide
  59
  60theorem ringdown_zip_entry_count_pos : 0 < ringdownZipEntryCount := by
  61  unfold ringdownZipEntryCount
  62  decide
  63
  64theorem ringdown_zip_extension_count_sum :
  65    ringdownZipH5Count + ringdownZipDirectoryMarkerCount = ringdownZipEntryCount := by
  66  unfold ringdownZipH5Count ringdownZipDirectoryMarkerCount ringdownZipEntryCount
  67  decide
  68
  69theorem ringdown_zip_top_level_count_eq_entries :
  70    ringdownZipTopLevelRinCount = ringdownZipEntryCount := by
  71  unfold ringdownZipTopLevelRinCount ringdownZipEntryCount
  72  rfl
  73
  74theorem ringdown_zip_total_uncompressed_gt_compressed :
  75    ringdownZipTotalCompressedSize < ringdownZipTotalUncompressedSize := by
  76  unfold ringdownZipTotalCompressedSize ringdownZipTotalUncompressedSize
  77  decide
  78
  79theorem ringdown_zip_cd_inside_source :
  80    ringdownZipCentralDirectoryOffset + ringdownZipCentralDirectorySize <
  81      ringdownZipSourceSizeBytes := by
  82  unfold ringdownZipCentralDirectoryOffset ringdownZipCentralDirectorySize
  83    ringdownZipSourceSizeBytes
  84  decide
  85
  86/-! ## §3. Master cert -/
  87
  88structure GWTC3RingdownZipSchemaCert where
  89  source_size_pos : 0 < ringdownZipSourceSizeBytes
  90  central_directory_size_pos : 0 < ringdownZipCentralDirectorySize
  91  entry_count_pos : 0 < ringdownZipEntryCount
  92  extension_count_sum :
  93    ringdownZipH5Count + ringdownZipDirectoryMarkerCount = ringdownZipEntryCount
  94  top_level_count_eq_entries :
  95    ringdownZipTopLevelRinCount = ringdownZipEntryCount
  96  total_uncompressed_gt_compressed :
  97    ringdownZipTotalCompressedSize < ringdownZipTotalUncompressedSize
  98  central_directory_inside_source :
  99    ringdownZipCentralDirectoryOffset + ringdownZipCentralDirectorySize <
 100      ringdownZipSourceSizeBytes
 101  ringdown_manifest_key :
 102    ringdownFile.key = "IGWN-GWTC3-TGR-v1-rin.zip"
 103
 104def gwtc3RingdownZipSchemaCert : GWTC3RingdownZipSchemaCert where
 105  source_size_pos := ringdown_zip_source_size_pos
 106  central_directory_size_pos := ringdown_zip_cd_size_pos
 107  entry_count_pos := ringdown_zip_entry_count_pos
 108  extension_count_sum := ringdown_zip_extension_count_sum
 109  top_level_count_eq_entries := ringdown_zip_top_level_count_eq_entries
 110  total_uncompressed_gt_compressed := ringdown_zip_total_uncompressed_gt_compressed
 111  central_directory_inside_source := ringdown_zip_cd_inside_source
 112  ringdown_manifest_key := ringdown_file_key
 113
 114theorem gwtc3RingdownZipSchemaCert_inhabited :
 115    Nonempty GWTC3RingdownZipSchemaCert :=
 116  ⟨gwtc3RingdownZipSchemaCert⟩
 117
 118/-- One-statement schema theorem for the ringdown ZIP. -/
 119theorem gwtc3_ringdown_zip_schema_one_statement :
 120    (ringdownZipEntryCount = 244) ∧
 121    (ringdownZipH5Count = 243) ∧
 122    (ringdownZipDirectoryMarkerCount = 1) ∧
 123    (ringdownZipH5Count + ringdownZipDirectoryMarkerCount = ringdownZipEntryCount) ∧
 124    (ringdownZipTopLevelRinCount = ringdownZipEntryCount) ∧
 125    (ringdownZipTotalCompressedSize < ringdownZipTotalUncompressedSize) ∧
 126    (ringdownFile.key = "IGWN-GWTC3-TGR-v1-rin.zip") ∧
 127    Nonempty GWTC3RingdownZipSchemaCert :=
 128  ⟨rfl, rfl, rfl,
 129   ringdown_zip_extension_count_sum,
 130   ringdown_zip_top_level_count_eq_entries,
 131   ringdown_zip_total_uncompressed_gt_compressed,
 132   ringdown_file_key,
 133   gwtc3RingdownZipSchemaCert_inhabited⟩
 134
 135end GWTC3RingdownZipSchema
 136end Verification
 137end IndisputableMonolith
 138