IndisputableMonolith.Gravity.BHEchoPerEventCatalog

   1import Mathlib
   2import IndisputableMonolith.Gravity.BHEchoesLIGOCatalog
   3
   4/-!
   5# Per-Event BH Echo Prediction Catalog
   6
   7The structural BH-echo cert (`Gravity/BHEchoesLIGOCatalog`) gives the
   8generic bounce-radius and echo-delay scaling. This module records the
   9per-event prediction tables for the four canonical headline LIGO/Virgo
  10events. For each event we name the source mass `M`, the recognition
  11rung `N`, the predicted echo delay `Δt(N)` in RS-native units, and
  12the predicted echo frequency `f_echo(N) = 1 / Δt(N)`.
  13
  14Per-event predictions (RS-native, dimensionless):
  15
  16| Event     | M (M☉)  | N | Δt(N)   | f_echo(N) |
  17|-----------|---------|---|---------|-----------|
  18| GW150914  | ~65     | 8 | 47·log φ | 1/(47 logφ) |
  19| GW170817  | ~2.7    | 1 | φ ·log φ | 1/(φ logφ)  |
  20| GW190521  | ~150    | 10| φ¹⁰·log φ| 1/(φ¹⁰ logφ)|
  21| GW230529  | ~4.4    | 2 | φ² ·log φ| 1/(φ² logφ) |
  22
  23Each prediction is `Δt > 0` and `f_echo > 0` strictly. Adjacent-rung
  24echo frequencies ratio by `1/φ`; the per-event ladder admits
  25falsification by any single high-SNR event whose echo signature does
  26not appear at the predicted rung.
  27
  28Lean status: 0 sorry, 0 axiom.
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Gravity
  33namespace BHEchoPerEventCatalog
  34
  35open Constants
  36open Gravity.BHEchoesLIGOCatalog
  37
  38noncomputable section
  39
  40/-- The four canonical LIGO/Virgo headline events. -/
  41inductive HeadlineEvent where
  42  | GW150914
  43  | GW170817
  44  | GW190521
  45  | GW230529
  46  deriving DecidableEq, Repr, BEq, Fintype
  47
  48/-- Predicted recognition rung for each headline event (chosen from
  49log-mass scaling: rung N ≈ ⌊log_φ(M / M_ref)⌋). -/
  50def predictedRung : HeadlineEvent → ℕ
  51  | .GW150914 => 8
  52  | .GW170817 => 1
  53  | .GW190521 => 10
  54  | .GW230529 => 2
  55
  56/-- Predicted bounce radius per event. -/
  57def predictedBounceRadius (e : HeadlineEvent) : ℝ :=
  58  bounceRadius (predictedRung e)
  59
  60/-- Predicted echo delay per event. -/
  61def predictedEchoDelay (e : HeadlineEvent) : ℝ :=
  62  echoDelay (predictedRung e)
  63
  64/-- Bounce radius per event is strictly positive. -/
  65theorem predictedBounceRadius_pos (e : HeadlineEvent) :
  66    0 < predictedBounceRadius e :=
  67  bounceRadius_pos _
  68
  69/-- Echo delay per event is strictly positive (every predicted rung is
  70N ≥ 1; verified by `decide` on the inductive cases). -/
  71theorem predictedEchoDelay_pos (e : HeadlineEvent) :
  72    0 < predictedEchoDelay e := by
  73  unfold predictedEchoDelay predictedRung
  74  cases e <;> exact echoDelay_pos _ (by decide)
  75
  76/-- Predicted echo frequency per event is `1 / Δt(N)`. -/
  77def predictedEchoFrequency (e : HeadlineEvent) : ℝ :=
  78  1 / predictedEchoDelay e
  79
  80theorem predictedEchoFrequency_pos (e : HeadlineEvent) :
  81    0 < predictedEchoFrequency e := by
  82  unfold predictedEchoFrequency
  83  exact div_pos one_pos (predictedEchoDelay_pos e)
  84
  85/-- Catalog count = 4. -/
  86theorem event_count : Fintype.card HeadlineEvent = 4 := by decide
  87
  88/-- The two largest events (GW190521 and GW150914) sit at higher rungs
  89than the two smaller (GW170817, GW230529). -/
  90theorem rung_ordering :
  91    predictedRung .GW170817 < predictedRung .GW230529 ∧
  92    predictedRung .GW230529 < predictedRung .GW150914 ∧
  93    predictedRung .GW150914 < predictedRung .GW190521 := by
  94  refine ⟨?_, ?_, ?_⟩ <;> decide
  95
  96structure BHEchoCatalogCert where
  97  event_count : Fintype.card HeadlineEvent = 4
  98  bounce_pos : ∀ e, 0 < predictedBounceRadius e
  99  delay_pos : ∀ e, 0 < predictedEchoDelay e
 100  freq_pos : ∀ e, 0 < predictedEchoFrequency e
 101  rung_ordering :
 102    predictedRung .GW170817 < predictedRung .GW230529 ∧
 103    predictedRung .GW230529 < predictedRung .GW150914 ∧
 104    predictedRung .GW150914 < predictedRung .GW190521
 105
 106/-- Per-event BH-echo catalog certificate. -/
 107def bhEchoCatalogCert : BHEchoCatalogCert where
 108  event_count := event_count
 109  bounce_pos := predictedBounceRadius_pos
 110  delay_pos := predictedEchoDelay_pos
 111  freq_pos := predictedEchoFrequency_pos
 112  rung_ordering := rung_ordering
 113
 114end
 115end BHEchoPerEventCatalog
 116end Gravity
 117end IndisputableMonolith
 118