IndisputableMonolith.Gravity.BHEchoAmplitudes

   1import Mathlib
   2import IndisputableMonolith.Gravity.BHEchoPerEventCatalog
   3
   4/-!
   5# Black-Hole Echo Amplitudes with Phi-Ladder Damping
   6
   7The echo-delay cert gives `Δt(N)` and frequency per event. This module
   8adds the amplitude prediction: each successive reflection off the bounce
   9surface is attenuated by a factor `φ⁻¹` (one φ-rung of recognition
  10cost), giving echo amplitudes `A_n = A_0 · φ^(-n)` for echo number `n`.
  11
  12The structural prediction: the SNR of the nth echo relative to the
  13(n-1)th echo is exactly 1/φ ≈ 0.618 for every LIGO/Virgo event.
  14Falsifier: post-processing of any high-SNR merger event that shows
  15either no echo or an echo-amplitude ratio systematically different from
  161/φ between successive echoes.
  17
  18This compounds with the existing catalog cert:
  19`Gravity/BHEchoPerEventCatalog`.
  20
  21Lean status: 0 sorry, 0 axiom.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Gravity
  26namespace BHEchoAmplitudes
  27
  28open Constants
  29open Gravity.BHEchoPerEventCatalog
  30
  31noncomputable section
  32
  33/-- Echo amplitude at reflection number `n` (relative to primary). -/
  34def echoAmplitude (n : ℕ) : ℝ := phi ^ (-(n : ℤ))
  35
  36theorem echoAmplitude_pos (n : ℕ) : 0 < echoAmplitude n :=
  37  zpow_pos Constants.phi_pos _
  38
  39theorem echoAmplitude_one : echoAmplitude 0 = 1 := by
  40  simp [echoAmplitude]
  41
  42/-- Each echo is attenuated by 1/φ relative to the previous. -/
  43theorem echoAmplitude_succ_ratio (n : ℕ) :
  44    echoAmplitude (n + 1) = echoAmplitude n * phi⁻¹ := by
  45  unfold echoAmplitude
  46  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  47  have : phi ^ (-((n : ℤ) + 1)) = phi ^ (-(n : ℤ)) * phi⁻¹ := by
  48    rw [show (-((n : ℤ) + 1)) = -(n : ℤ) + (-1 : ℤ) by ring]
  49    rw [zpow_add₀ hphi_ne]; simp
  50  have hcast : ((n + 1 : ℕ) : ℤ) = (n : ℤ) + 1 := by push_cast; ring
  51  rw [hcast, this]
  52
  53/-- SNR ratio between successive echoes = 1/φ. -/
  54theorem echo_snr_ratio (n : ℕ) :
  55    echoAmplitude (n + 1) / echoAmplitude n = phi⁻¹ := by
  56  rw [echoAmplitude_succ_ratio]
  57  field_simp [(echoAmplitude_pos n).ne']
  58
  59/-- Amplitudes are strictly decreasing. -/
  60theorem echoAmplitude_strictly_decreasing (n : ℕ) :
  61    echoAmplitude (n + 1) < echoAmplitude n := by
  62  rw [echoAmplitude_succ_ratio]
  63  have hn : 0 < echoAmplitude n := echoAmplitude_pos n
  64  have : phi⁻¹ < 1 :=
  65    inv_lt_one_of_one_lt₀ (by have := Constants.phi_gt_onePointFive; linarith)
  66  linarith [mul_lt_iff_lt_one_right hn |>.mpr this]
  67
  68/-- Per-event echo-amplitude chain for catalog events. -/
  69def catalogAmplitude
  70    (e : HeadlineEvent) (n : ℕ) : ℝ := echoAmplitude n
  71
  72theorem catalogAmplitude_pos (e : HeadlineEvent) (n : ℕ) :
  73    0 < catalogAmplitude e n := echoAmplitude_pos n
  74
  75structure BHEchoAmplitudeCert where
  76  amplitude_pos : ∀ n, 0 < echoAmplitude n
  77  primary_unity : echoAmplitude 0 = 1
  78  one_step_ratio : ∀ n, echoAmplitude (n + 1) = echoAmplitude n * phi⁻¹
  79  snr_ratio : ∀ n, echoAmplitude (n + 1) / echoAmplitude n = phi⁻¹
  80  strictly_decreasing : ∀ n, echoAmplitude (n + 1) < echoAmplitude n
  81  catalog_pos : ∀ (e : HeadlineEvent) n, 0 < catalogAmplitude e n
  82
  83/-- BH-echo amplitude certificate. -/
  84def bhEchoAmplitudeCert : BHEchoAmplitudeCert where
  85  amplitude_pos := echoAmplitude_pos
  86  primary_unity := echoAmplitude_one
  87  one_step_ratio := echoAmplitude_succ_ratio
  88  snr_ratio := echo_snr_ratio
  89  strictly_decreasing := echoAmplitude_strictly_decreasing
  90  catalog_pos := catalogAmplitude_pos
  91
  92end
  93end BHEchoAmplitudes
  94end Gravity
  95end IndisputableMonolith
  96