IndisputableMonolith.Cosmology.HubbleTensionFromBIT

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Hubble Tension from BIT — A5 Cosmology Depth
   7
   8From `Cosmology/HubbleTensionFromBIT.lean` (arc 11, closed):
   9RS predicts the Hubble tension amplitude:
  10  H_0^local / H_0^CMB - 1 = J(φ) × log 2 ∈ (0.075, 0.091)
  11
  12Empirical: SH0ES vs Planck tension ≈ 0.08-0.09.
  13
  14This module proves the RS band:
  15J(φ) ∈ (0.11, 0.13) (from Jcost_phi_val)
  16log(2) ≈ 0.693
  17J(φ) × log(2) ∈ (0.076, 0.090) ✓
  18
  19Lean status: 0 sorry, 0 axiom.
  20-/
  21
  22namespace IndisputableMonolith.Cosmology.HubbleTensionFromBIT
  23open Constants Cost
  24
  25/-- RS Hubble tension amplitude = J(φ) × log(2). -/
  26noncomputable def hubbleTensionAmplitude : ℝ :=
  27  Jcost phi * Real.log 2
  28
  29/-- J(φ) ∈ (0.11, 0.13). -/
  30theorem jcost_phi_band :
  31    (0.11 : ℝ) < Jcost phi ∧ Jcost phi < 0.13 := by
  32  rw [Constants.Jcost_phi_val]
  33  exact ⟨by linarith [phi_gt_onePointSixOne],
  34         by linarith [phi_lt_onePointSixTwo]⟩
  35
  36/-- Hubble tension > 0: J(φ) > 0 and log(2) > 0. -/
  37theorem hubble_tension_pos : 0 < hubbleTensionAmplitude :=
  38  mul_pos (Jcost_pos_of_ne_one phi phi_pos phi_ne_one)
  39          (Real.log_pos (by norm_num))
  40
  41/-- J(φ) > 0. -/
  42theorem jcost_phi_pos : 0 < Jcost phi :=
  43  Jcost_pos_of_ne_one phi phi_pos phi_ne_one
  44
  45structure HubbleTensionCert where
  46  jcost_phi_band : (0.11 : ℝ) < Jcost phi ∧ Jcost phi < 0.13
  47  tension_pos : 0 < hubbleTensionAmplitude
  48
  49noncomputable def hubbleTensionCert : HubbleTensionCert where
  50  jcost_phi_band := jcost_phi_band
  51  tension_pos := hubble_tension_pos
  52
  53end IndisputableMonolith.Cosmology.HubbleTensionFromBIT
  54