IndisputableMonolith.Verification.Preregistered.Hubble.Test

   1import Mathlib
   2import IndisputableMonolith.Verification.Preregistered.Core
   3import IndisputableMonolith.Verification.Preregistered.Hubble.Prediction
   4import IndisputableMonolith.Verification.Preregistered.Hubble.Measurement_2022
   5import IndisputableMonolith.Physics.CKMGeometry
   6import IndisputableMonolith.Constants.Alpha
   7
   8/-!
   9# Tests: Hubble ratio (relative error) and Ω_Λ (within 1σ)
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Verification
  14namespace Preregistered
  15namespace Hubble
  16
  17open Preregistered
  18open IndisputableMonolith.Constants
  19
  20/-- Hubble test: RS ratio predicts late from early within 0.05% relative error. -/
  21theorem hubble_ratio_passes_rel_0p05pct :
  22    abs (H_early * hubble_ratio.val - H_late) / H_late < 0.0005 := by
  23  -- Pure arithmetic check with the measurement module’s numbers.
  24  simp [H_early, H_late, hubble_ratio]
  25  norm_num
  26
  27/-! Ω_Λ test needs a small bound on α/π, derived from existing α bounds. -/
  28
  29theorem alpha_over_pi_bounds :
  30    (0.0023 : ℝ) < alpha / Real.pi ∧ alpha / Real.pi < (0.0024 : ℝ) := by
  31  have h_alpha_lower := Physics.CKMGeometry.alpha_lower_bound
  32  have h_alpha_upper := Physics.CKMGeometry.alpha_upper_bound
  33  have h_pi_lower : (3.14 : ℝ) < Real.pi := by linarith [Real.pi_gt_d6]
  34  have h_pi_upper : Real.pi < (3.15 : ℝ) := by linarith [Real.pi_lt_d6]
  35  have h_alpha_pos : 0 < alpha := lt_trans (by norm_num) h_alpha_lower
  36  have h_pi_pos : 0 < Real.pi := Real.pi_pos
  37  constructor
  38  · -- Lower bound: 0.0023 < alpha/pi
  39    calc (0.0023 : ℝ) < 0.00729 / 3.15 := by norm_num
  40      _ < alpha / 3.15 := by
  41          apply div_lt_div_of_pos_right h_alpha_lower
  42          norm_num
  43      _ < alpha / Real.pi := by
  44          apply div_lt_div_of_pos_left h_alpha_pos h_pi_pos
  45          exact h_pi_upper
  46  · -- Upper bound: alpha/pi < 0.0024
  47    calc alpha / Real.pi < alpha / 3.14 := by
  48          apply div_lt_div_of_pos_left h_alpha_pos (by norm_num) h_pi_lower
  49      _ < 0.00731 / 3.14 := by
  50          apply div_lt_div_of_pos_right h_alpha_upper
  51          norm_num
  52      _ < (0.0024 : ℝ) := by norm_num
  53
  54theorem omega_lambda_passes_1sigma :
  55    within_sigma omega_lambda omega_lambda_measurement := by
  56  unfold Preregistered.within_sigma
  57  -- Expand only the measurement payload; keep `alpha` opaque (do NOT simp-unfold it).
  58  simp [omega_lambda_measurement]
  59  -- Freeze the prediction formula in a stable, human-readable form:
  60  change |((11 : ℝ) / 16 - alpha / Real.pi) - 0.6847| < (0.0073 : ℝ)
  61  have h_ap := alpha_over_pi_bounds
  62  -- `omega_lambda.val = 0.6875 - alpha/pi` and alpha/pi ∈ (0.0023, 0.0024)
  63  have h_pred_lower : (0.6851 : ℝ) < (11 : ℝ) / 16 - alpha / Real.pi := by
  64    have h2 : (11 : ℝ) / 16 = (0.6875 : ℝ) := by norm_num
  65    linarith [h_ap.2, h2]
  66  have h_pred_upper : (11 : ℝ) / 16 - alpha / Real.pi < (0.6852 : ℝ) := by
  67    have h2 : (11 : ℝ) / 16 = (0.6875 : ℝ) := by norm_num
  68    linarith [h_ap.1, h2]
  69  -- Since pred > 0.6851 > 0.6847, the difference is positive, so `abs` drops.
  70  have hpos : (0 : ℝ) < ((11 : ℝ) / 16 - alpha / Real.pi) - 0.6847 := by
  71    have : (0.6851 : ℝ) < (11 : ℝ) / 16 - alpha / Real.pi := h_pred_lower
  72    linarith
  73  have habs :
  74      |((11 : ℝ) / 16 - alpha / Real.pi) - 0.6847| =
  75        ((11 : ℝ) / 16 - alpha / Real.pi) - 0.6847 :=
  76    abs_of_pos hpos
  77  rw [habs]
  78  have hsmall : ((11 : ℝ) / 16 - alpha / Real.pi) - 0.6847 < (0.0073 : ℝ) := by
  79    have : (11 : ℝ) / 16 - alpha / Real.pi < (0.6852 : ℝ) := h_pred_upper
  80    linarith
  81  exact hsmall
  82
  83end Hubble
  84end Preregistered
  85end Verification
  86end IndisputableMonolith
  87