IndisputableMonolith.Verification.GWTC3RingdownLikelihoodSelector

   1import Mathlib
   2import IndisputableMonolith.Verification.GWTC3RingdownFamilyComparison
   3import IndisputableMonolith.Verification.GWTC3RingdownFilenameTaxonomy
   4
   5/-!
   6# GWTC-3 Ringdown Family-Stratified Likelihood Selector
   7
   8## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   9
  10This module records the selector policy for future GWTC-3 ringdown
  11likelihoods.
  12
  13Mapped / eligible families:
  14
  15* `DS_1mode_10M` — direct `f_t_0` / `tau_t_0` damping mapping.
  16* `Kerr_220_0M` — Kerr 220 quality-factor mapping at 0M start.
  17* `Kerr_220_10M` — Kerr 220 quality-factor mapping at 10M start.
  18
  19Blocked families:
  20
  21* every `Kerr_221*` family until a 221-mode mapping is formalized;
  22* every `MMRDNP*` family until its observable mapping is formalized;
  23* `pseobnrv4hm` until waveform-family semantics are formalized.
  24
  25Counts:
  26
  27* total HDF5 files: `243`
  28* eligible files: `66`
  29* blocked files: `177`
  30* total model families: `14`
  31* eligible model families: `3`
  32* blocked model families: `11`
  33
  34This is selector policy only. It computes no posterior likelihood.
  35Zero `sorry`. Zero new RS-specific axioms.
  36-/
  37
  38namespace IndisputableMonolith
  39namespace Verification
  40namespace GWTC3RingdownLikelihoodSelector
  41
  42open IndisputableMonolith.Verification.GWTC3RingdownFilenameTaxonomy
  43open IndisputableMonolith.Verification.GWTC3RingdownFamilyComparison
  44
  45/-! ## §1. Selector counts -/
  46
  47def selectorTotalHDF5Files : Nat := 243
  48def selectorEligibleFiles : Nat := 66
  49def selectorBlockedFiles : Nat := 177
  50def selectorTotalModels : Nat := 14
  51def selectorEligibleModels : Nat := 3
  52def selectorBlockedModels : Nat := 11
  53def selectorNoMixedAggregation : Bool := true
  54
  55/-! ## §2. Arithmetic facts -/
  56
  57theorem selector_file_count_partition :
  58    selectorEligibleFiles + selectorBlockedFiles = selectorTotalHDF5Files := by
  59  unfold selectorEligibleFiles selectorBlockedFiles selectorTotalHDF5Files
  60  decide
  61
  62theorem selector_model_count_partition :
  63    selectorEligibleModels + selectorBlockedModels = selectorTotalModels := by
  64  unfold selectorEligibleModels selectorBlockedModels selectorTotalModels
  65  decide
  66
  67theorem selector_eligible_files_match_comparison :
  68    selectorEligibleFiles = comparisonTotalMembers := rfl
  69
  70theorem selector_total_files_match_taxonomy :
  71    selectorTotalHDF5Files = taxonomyHDF5FileCount := rfl
  72
  73theorem selector_has_blocked_files :
  74    0 < selectorBlockedFiles := by
  75  unfold selectorBlockedFiles
  76  decide
  77
  78theorem selector_no_mixed_aggregation_true :
  79    selectorNoMixedAggregation = true := rfl
  80
  81/-! ## §3. Master cert -/
  82
  83structure GWTC3RingdownLikelihoodSelectorCert where
  84  file_count_partition :
  85    selectorEligibleFiles + selectorBlockedFiles = selectorTotalHDF5Files
  86  model_count_partition :
  87    selectorEligibleModels + selectorBlockedModels = selectorTotalModels
  88  eligible_files_match_comparison :
  89    selectorEligibleFiles = comparisonTotalMembers
  90  total_files_match_taxonomy :
  91    selectorTotalHDF5Files = taxonomyHDF5FileCount
  92  has_blocked_files :
  93    0 < selectorBlockedFiles
  94  no_mixed_aggregation :
  95    selectorNoMixedAggregation = true
  96  comparison_available :
  97    Nonempty GWTC3RingdownFamilyComparisonCert
  98  taxonomy_available :
  99    Nonempty GWTC3RingdownFilenameTaxonomyCert
 100
 101def gwtc3RingdownLikelihoodSelectorCert :
 102    GWTC3RingdownLikelihoodSelectorCert where
 103  file_count_partition := selector_file_count_partition
 104  model_count_partition := selector_model_count_partition
 105  eligible_files_match_comparison := selector_eligible_files_match_comparison
 106  total_files_match_taxonomy := selector_total_files_match_taxonomy
 107  has_blocked_files := selector_has_blocked_files
 108  no_mixed_aggregation := selector_no_mixed_aggregation_true
 109  comparison_available := gwtc3RingdownFamilyComparisonCert_inhabited
 110  taxonomy_available := gwtc3RingdownFilenameTaxonomyCert_inhabited
 111
 112theorem gwtc3RingdownLikelihoodSelectorCert_inhabited :
 113    Nonempty GWTC3RingdownLikelihoodSelectorCert :=
 114  ⟨gwtc3RingdownLikelihoodSelectorCert⟩
 115
 116/-- One-statement selector theorem. -/
 117theorem gwtc3_ringdown_likelihood_selector_one_statement :
 118    (selectorTotalHDF5Files = 243) ∧
 119    (selectorEligibleFiles = 66) ∧
 120    (selectorBlockedFiles = 177) ∧
 121    (selectorTotalModels = 14) ∧
 122    (selectorEligibleModels = 3) ∧
 123    (selectorBlockedModels = 11) ∧
 124    (selectorNoMixedAggregation = true) ∧
 125    Nonempty GWTC3RingdownLikelihoodSelectorCert :=
 126  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl,
 127   gwtc3RingdownLikelihoodSelectorCert_inhabited⟩
 128
 129end GWTC3RingdownLikelihoodSelector
 130end Verification
 131end IndisputableMonolith
 132