IndisputableMonolith.Verification.GWTC3RingdownGuardedFamilyScripts

   1import Mathlib
   2import IndisputableMonolith.Verification.GWTC3RingdownFamilyGuard
   3import IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily
   4import IndisputableMonolith.Verification.GWTC3RingdownKerr2200MDampingFamily
   5import IndisputableMonolith.Verification.GWTC3RingdownKerr22010MDampingFamily
   6
   7/-!
   8# GWTC-3 Ringdown Guarded Family Scripts
   9
  10## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
  11
  12This module records Session 133: the runtime family guard is now wired
  13into the mapped family-statistic scripts.
  14
  15Patched scripts:
  16
  17* `gwtc3_ringdown_ds1mode10m_damping_family.py`
  18* `gwtc3_ringdown_kerr2200m_damping_family.py`
  19* `gwtc3_ringdown_kerr22010m_damping_family.py`
  20
  21Each script now calls `require_eligible_model(MODEL)` before reading
  22posterior data. A smoke test confirms eligible families pass and
  23representative blocked/unknown families fail.
  24
  25This is operational guarding only. It adds no new physics mapping and
  26computes no new likelihood.
  27Zero `sorry`. Zero new RS-specific axioms.
  28-/
  29
  30namespace IndisputableMonolith
  31namespace Verification
  32namespace GWTC3RingdownGuardedFamilyScripts
  33
  34open IndisputableMonolith.Verification.GWTC3RingdownFamilyGuard
  35open IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily
  36open IndisputableMonolith.Verification.GWTC3RingdownKerr2200MDampingFamily
  37open IndisputableMonolith.Verification.GWTC3RingdownKerr22010MDampingFamily
  38
  39/-! ## §1. Guarded script counts -/
  40
  41def guardedScriptCount : Nat := 3
  42def smokeTestCount : Nat := 7
  43def smokePassCount : Nat := 7
  44def smokeAllPassed : Bool := true
  45
  46theorem guarded_script_count_matches_selector :
  47    guardedScriptCount = guardEligibleModelCount := rfl
  48
  49theorem smoke_all_passed : smokeAllPassed = true := rfl
  50
  51theorem smoke_pass_count_eq_test_count :
  52    smokePassCount = smokeTestCount := rfl
  53
  54/-! ## §2. Guard accepts mapped scripts -/
  55
  56theorem guarded_DS_script_accepted :
  57    guardModel "DS_1mode_10M" = .accept :=
  58  guard_accepts_DS
  59
  60theorem guarded_Kerr2200_script_accepted :
  61    guardModel "Kerr_220_0M" = .accept :=
  62  guard_accepts_Kerr2200
  63
  64theorem guarded_Kerr22010_script_accepted :
  65    guardModel "Kerr_220_10M" = .accept :=
  66  guard_accepts_Kerr22010
  67
  68theorem representative_blocked_rejected :
  69    guardModel "Kerr_221_0M" = .reject ∧
  70    guardModel "MMRDNP_10M" = .reject ∧
  71    guardModel "pseobnrv4hm" = .reject :=
  72  ⟨guard_rejects_Kerr2210, guard_rejects_MMRDNP, guard_rejects_pseobnrv4hm⟩
  73
  74/-! ## §3. Master cert -/
  75
  76structure GWTC3RingdownGuardedFamilyScriptsCert where
  77  guarded_count :
  78    guardedScriptCount = guardEligibleModelCount
  79  smoke_passed :
  80    smokeAllPassed = true
  81  smoke_count :
  82    smokePassCount = smokeTestCount
  83  DS_script_accepted :
  84    guardModel "DS_1mode_10M" = .accept
  85  Kerr2200_script_accepted :
  86    guardModel "Kerr_220_0M" = .accept
  87  Kerr22010_script_accepted :
  88    guardModel "Kerr_220_10M" = .accept
  89  blocked_rejected :
  90    guardModel "Kerr_221_0M" = .reject ∧
  91    guardModel "MMRDNP_10M" = .reject ∧
  92    guardModel "pseobnrv4hm" = .reject
  93  DS_cert_available :
  94    Nonempty GWTC3RingdownDS1Mode10MDampingFamilyCert
  95  Kerr2200_cert_available :
  96    Nonempty GWTC3RingdownKerr2200MDampingFamilyCert
  97  Kerr22010_cert_available :
  98    Nonempty GWTC3RingdownKerr22010MDampingFamilyCert
  99  guard_cert_available :
 100    Nonempty GWTC3RingdownFamilyGuardCert
 101
 102def gwtc3RingdownGuardedFamilyScriptsCert :
 103    GWTC3RingdownGuardedFamilyScriptsCert where
 104  guarded_count := guarded_script_count_matches_selector
 105  smoke_passed := smoke_all_passed
 106  smoke_count := smoke_pass_count_eq_test_count
 107  DS_script_accepted := guarded_DS_script_accepted
 108  Kerr2200_script_accepted := guarded_Kerr2200_script_accepted
 109  Kerr22010_script_accepted := guarded_Kerr22010_script_accepted
 110  blocked_rejected := representative_blocked_rejected
 111  DS_cert_available := gwtc3RingdownDS1Mode10MDampingFamilyCert_inhabited
 112  Kerr2200_cert_available := gwtc3RingdownKerr2200MDampingFamilyCert_inhabited
 113  Kerr22010_cert_available := gwtc3RingdownKerr22010MDampingFamilyCert_inhabited
 114  guard_cert_available := gwtc3RingdownFamilyGuardCert_inhabited
 115
 116theorem gwtc3RingdownGuardedFamilyScriptsCert_inhabited :
 117    Nonempty GWTC3RingdownGuardedFamilyScriptsCert :=
 118  ⟨gwtc3RingdownGuardedFamilyScriptsCert⟩
 119
 120/-- One-statement theorem for the guarded family scripts. -/
 121theorem gwtc3_ringdown_guarded_family_scripts_one_statement :
 122    (guardedScriptCount = 3) ∧
 123    (smokeTestCount = 7) ∧
 124    (smokePassCount = 7) ∧
 125    (smokeAllPassed = true) ∧
 126    (guardModel "DS_1mode_10M" = .accept) ∧
 127    (guardModel "Kerr_220_0M" = .accept) ∧
 128    (guardModel "Kerr_220_10M" = .accept) ∧
 129    Nonempty GWTC3RingdownGuardedFamilyScriptsCert :=
 130  ⟨rfl, rfl, rfl, rfl,
 131   guard_accepts_DS,
 132   guard_accepts_Kerr2200,
 133   guard_accepts_Kerr22010,
 134   gwtc3RingdownGuardedFamilyScriptsCert_inhabited⟩
 135
 136end GWTC3RingdownGuardedFamilyScripts
 137end Verification
 138end IndisputableMonolith
 139