IndisputableMonolith.Cosmology.BITKernelFamilies

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# BIT Kernel Families for w(z) Forecasting
   6
   7Three kernel-family models for the BIT cosmic-Z-aging amplitude
   8`δw(z) = δw_0 · K(z)`:
   9
  10  K1: K(z) = 1                 (constant)
  11  K2: K(z) = 1 / (1 + z)       (canonical RS arc-11 kernel)
  12  K3: K(z) = exp(-z / z_0)     (exponential)
  13
  14Each kernel is bounded in `[0, 1]` on `z ≥ 0`, and the maximum
  15amplitude `δw_0 ∈ [0, J(φ)]` from the BIT theorem (§XXIV).
  16
  17Used by `scripts/analysis/desi_y3_wz_forecast.py` for the DESI Y3
  18forecast.
  19-/
  20
  21namespace IndisputableMonolith
  22namespace Cosmology
  23namespace BITKernelFamilies
  24
  25open IndisputableMonolith.Constants
  26
  27noncomputable section
  28
  29/-- Kernel family tag. -/
  30inductive KernelFamily where
  31  | constant_kernel
  32  | inv_one_plus_z
  33  | exponential
  34  deriving DecidableEq, Inhabited
  35
  36namespace KernelFamily
  37
  38def name : KernelFamily → String
  39  | constant_kernel  => "K1 (constant)"
  40  | inv_one_plus_z   => "K2 (1/(1+z))"
  41  | exponential      => "K3 (exp(-z/z0))"
  42
  43end KernelFamily
  44
  45/-- The BIT kernel function. -/
  46def kernel (k : KernelFamily) (z : ℝ) (z0 : ℝ := 1) : ℝ :=
  47  match k with
  48  | KernelFamily.constant_kernel  => 1
  49  | KernelFamily.inv_one_plus_z   => 1 / (1 + z)
  50  | KernelFamily.exponential      => Real.exp (- z / z0)
  51
  52/-- All three kernels equal 1 at `z = 0`. -/
  53theorem kernel_at_zero (k : KernelFamily) (z0 : ℝ) :
  54    kernel k 0 z0 = 1 := by
  55  cases k <;> simp [kernel]
  56
  57/-- The constant kernel is `1` everywhere. -/
  58theorem constant_kernel_eq_one (z z0 : ℝ) :
  59    kernel KernelFamily.constant_kernel z z0 = 1 := rfl
  60
  61/-- The 1/(1+z) kernel is positive for `z > -1`. -/
  62theorem inv_one_plus_z_pos (z : ℝ) (h : -1 < z) (z0 : ℝ) :
  63    0 < kernel KernelFamily.inv_one_plus_z z z0 := by
  64  unfold kernel
  65  exact div_pos one_pos (by linarith)
  66
  67/-- The exponential kernel is positive everywhere. -/
  68theorem exp_kernel_pos (z z0 : ℝ) :
  69    0 < kernel KernelFamily.exponential z z0 := by
  70  unfold kernel
  71  exact Real.exp_pos _
  72
  73/-- The maximum BIT amplitude is `J(φ) = φ - 3/2 ≈ 0.118`. -/
  74def delta_w0_max : ℝ := phi - 3 / 2
  75
  76theorem delta_w0_max_pos : 0 < delta_w0_max := by
  77  unfold delta_w0_max
  78  have := phi_gt_onePointFive
  79  linarith
  80
  81theorem delta_w0_max_lt_one : delta_w0_max < 1 := by
  82  unfold delta_w0_max
  83  have := phi_lt_two
  84  linarith
  85
  86/-- The effective equation of state under BIT. -/
  87def w_eff (k : KernelFamily) (z delta_w0 : ℝ) (z0 : ℝ := 1) : ℝ :=
  88  -1 + delta_w0 * kernel k z z0
  89
  90/-- At `z = 0`, `w_eff = -1 + δw_0` for any kernel. -/
  91theorem w_eff_at_zero (k : KernelFamily) (delta_w0 z0 : ℝ) :
  92    w_eff k 0 delta_w0 z0 = -1 + delta_w0 := by
  93  unfold w_eff
  94  rw [kernel_at_zero]
  95  ring
  96
  97/-! ## Master certificate -/
  98
  99/-- **BIT KERNEL FAMILIES MASTER CERTIFICATE.** -/
 100structure BITKernelFamiliesCert where
 101  kernel_at_zero_one :
 102    ∀ k : KernelFamily, ∀ z0 : ℝ, kernel k 0 z0 = 1
 103  delta_w0_max_pos :
 104    0 < delta_w0_max
 105  delta_w0_max_lt_one :
 106    delta_w0_max < 1
 107  w_eff_at_zero :
 108    ∀ k : KernelFamily, ∀ (delta_w0 z0 : ℝ),
 109      w_eff k 0 delta_w0 z0 = -1 + delta_w0
 110
 111/-- The master certificate is inhabited. -/
 112def bitKernelFamiliesCert : BITKernelFamiliesCert where
 113  kernel_at_zero_one := kernel_at_zero
 114  delta_w0_max_pos := delta_w0_max_pos
 115  delta_w0_max_lt_one := delta_w0_max_lt_one
 116  w_eff_at_zero := w_eff_at_zero
 117
 118end
 119
 120end BITKernelFamilies
 121end Cosmology
 122end IndisputableMonolith
 123