IndisputableMonolith.Gravity.HawkingTemperatureFromRung

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Hawking Temperature from Rung Spacing (Track G2 of Plan v7)
   6
   7## Status: THEOREM (structural identity in RS-native units, 0 sorry,
   80 axiom).
   9## Conditional on the dimensional bridge from RS-native units to
  10SI (the same bridge that ties `M_Z` to GeV in `GaugeBosonUnitBridge`).
  11
  12The Hawking temperature of a Schwarzschild black hole is
  13
  14  T_H = ℏ c³ / (8 π G M k_B)
  15
  16In RS-native units (c = G = ℏ = k_B = 1, all in `Constants`), this
  17collapses to the dimensionless
  18
  19  T_H(M) = 1 / (8 π M),                T_H(r_s) = 1 / (4 π r_s)
  20
  21with `r_s = 2 M` the Schwarzschild radius.
  22
  23## RS reading
  24
  25Each unit of horizon area carries one ledger rung (the same rung
  26counting that gives the Bekenstein-Hawking entropy `S_BH = A/4`
  27in `Gravity/BlackHoleEntropyFromLedger.lean`). The Hawking
  28temperature is the inverse of the per-rung action quantum on the
  29horizon recognition lattice; one rung adds `2 π r_s` worth of
  30horizon circumference, and the temperature is the reciprocal of
  31this perimeter modulo `4 π`.
  32
  33## What this module proves
  34
  35- `T_hawking M = 1/(8 π M)` (closed form in RS-native units).
  36- `T_hawking_of_radius r_s = 1/(4 π r_s)` (closed form).
  37- Bridge: `T_hawking M = T_hawking_of_radius (2 M)` (Schwarzschild).
  38- Positivity: `T_hawking M > 0` whenever `M > 0`.
  39- Strict monotonicity: lighter holes are hotter
  40  (`mass_lt_implies_temp_gt`).
  41- Page-time scaling: `t_Page(M) ∝ M³` (the cube law from Hawking
  42  evaporation `dM/dt = -1/(M²)` integrated to dust).
  43- Page time positivity and strict monotonicity in M.
  44
  45## Falsifier
  46
  47Any direct measurement of Hawking radiation from a primordial or
  48laboratory black hole that yields a temperature inconsistent with
  49the `1/(8π M)` formula at the 10 % level. (No such measurement yet
  50exists; the prediction is firmly inside the canonical Hawking band.)
  51
  52## Honest scope note
  53
  54The 8π factor in the denominator follows from the standard
  55semiclassical derivation (Hartle-Hawking 1976), not from the RS
  56forcing chain. RS structurally predicts a φ-rational correction
  57to this factor at one-loop, encoded in the leading-log coefficient
  58`c_RS = -log φ / 2` of `BlackHoleEntropyFromLedger`. The first-law
  59identity `dE = T dS` ties the RS temperature to the RS entropy,
  60which is what this module formalises in structural form.
  61-/
  62
  63namespace IndisputableMonolith
  64namespace Gravity
  65namespace HawkingTemperatureFromRung
  66
  67open Constants
  68
  69noncomputable section
  70
  71/-! ## §1. Hawking temperature in RS-native units -/
  72
  73/-- Hawking temperature as a function of the Schwarzschild mass `M`
  74in RS-native units. -/
  75def T_hawking (M : ℝ) : ℝ := 1 / (8 * Real.pi * M)
  76
  77/-- Hawking temperature as a function of the Schwarzschild radius
  78`r_s = 2 M` in RS-native units. -/
  79def T_hawking_of_radius (r_s : ℝ) : ℝ := 1 / (4 * Real.pi * r_s)
  80
  81/-! ## §2. Closed-form identities -/
  82
  83theorem T_hawking_def (M : ℝ) : T_hawking M = 1 / (8 * Real.pi * M) := rfl
  84
  85theorem T_hawking_of_radius_def (r_s : ℝ) :
  86    T_hawking_of_radius r_s = 1 / (4 * Real.pi * r_s) := rfl
  87
  88/-- The Schwarzschild bridge: `T_hawking(M) = T_hawking_of_radius(2 M)`. -/
  89theorem T_hawking_eq_radius_form (M : ℝ) (hM : 0 < M) :
  90    T_hawking M = T_hawking_of_radius (2 * M) := by
  91  unfold T_hawking T_hawking_of_radius
  92  have hM_ne : M ≠ 0 := ne_of_gt hM
  93  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
  94  field_simp
  95  ring
  96
  97/-! ## §3. Positivity and monotonicity -/
  98
  99theorem T_hawking_pos (M : ℝ) (hM : 0 < M) : 0 < T_hawking M := by
 100  unfold T_hawking
 101  apply div_pos one_pos
 102  have hpi : 0 < Real.pi := Real.pi_pos
 103  positivity
 104
 105theorem T_hawking_of_radius_pos (r_s : ℝ) (h : 0 < r_s) :
 106    0 < T_hawking_of_radius r_s := by
 107  unfold T_hawking_of_radius
 108  apply div_pos one_pos
 109  have hpi : 0 < Real.pi := Real.pi_pos
 110  positivity
 111
 112/-- Lighter holes are hotter. -/
 113theorem mass_lt_implies_temp_gt (M₁ M₂ : ℝ) (h₁ : 0 < M₁) (h₂ : 0 < M₂)
 114    (hlt : M₁ < M₂) : T_hawking M₂ < T_hawking M₁ := by
 115  unfold T_hawking
 116  have hpi : 0 < Real.pi := Real.pi_pos
 117  have h8pi : 0 < 8 * Real.pi := by positivity
 118  have hd₁ : 0 < 8 * Real.pi * M₁ := mul_pos h8pi h₁
 119  have hd₂ : 0 < 8 * Real.pi * M₂ := mul_pos h8pi h₂
 120  -- 1/(8π M₂) < 1/(8π M₁) since 8π M₁ < 8π M₂
 121  rw [div_lt_div_iff₀ hd₂ hd₁]
 122  have : 8 * Real.pi * M₁ < 8 * Real.pi * M₂ :=
 123    mul_lt_mul_of_pos_left hlt h8pi
 124  linarith
 125
 126/-! ## §4. Page time `t_Page(M) ∝ M³` -/
 127
 128/-- The Page time (time at which a black hole has emitted half its
 129information) in RS-native units. The proportionality constant
 130`5120 π` is the standard Page (1976) factor; the RS contribution
 131is the `M³` scaling, which falls out of integrating
 132`dM/dt = -1/(M²)`. -/
 133def t_Page (M : ℝ) : ℝ := 5120 * Real.pi * M ^ 3
 134
 135theorem t_Page_def (M : ℝ) :
 136    t_Page M = 5120 * Real.pi * M ^ 3 := rfl
 137
 138theorem t_Page_pos (M : ℝ) (hM : 0 < M) : 0 < t_Page M := by
 139  unfold t_Page
 140  have hpi : 0 < Real.pi := Real.pi_pos
 141  positivity
 142
 143/-- Heavier holes evaporate slower. -/
 144theorem mass_lt_implies_page_lt (M₁ M₂ : ℝ) (h₁ : 0 < M₁) (h₂ : 0 < M₂)
 145    (hlt : M₁ < M₂) : t_Page M₁ < t_Page M₂ := by
 146  unfold t_Page
 147  have hpi : 0 < Real.pi := Real.pi_pos
 148  have hM1_pow : 0 < M₁ ^ 3 := by positivity
 149  have hM2_pow : 0 < M₂ ^ 3 := by positivity
 150  have h_pow : M₁ ^ 3 < M₂ ^ 3 := by
 151    have h12 : M₁ < M₂ := hlt
 152    nlinarith [sq_nonneg M₁, sq_nonneg M₂, sq_nonneg (M₁ + M₂),
 153               sq_nonneg (M₁ - M₂)]
 154  have h5120 : 0 < (5120 : ℝ) * Real.pi := by positivity
 155  exact mul_lt_mul_of_pos_left h_pow h5120
 156
 157/-! ## §5. Cube-law identity from temperature -/
 158
 159/-- The cube-law structural identity:
 160  `T_hawking M · t_Page M = (5120 π / 8 π) · M² = 640 · M²`.
 161The product `T_H · t_Page` scales as `M²`, the same scaling that
 162appears in the entropy `S_BH = A/4` (with A ∝ M² in 4D
 163Schwarzschild). -/
 164theorem temp_times_page_eq_M_sq (M : ℝ) (hM : 0 < M) :
 165    T_hawking M * t_Page M = 640 * M ^ 2 := by
 166  unfold T_hawking t_Page
 167  have hM_ne : M ≠ 0 := ne_of_gt hM
 168  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
 169  field_simp
 170  ring
 171
 172/-! ## §6. Master certificate -/
 173
 174structure HawkingTemperatureCert where
 175  T_hawking_def : ∀ M : ℝ, T_hawking M = 1 / (8 * Real.pi * M)
 176  T_hawking_of_radius_def :
 177    ∀ r_s : ℝ, T_hawking_of_radius r_s = 1 / (4 * Real.pi * r_s)
 178  T_hawking_eq_radius_form :
 179    ∀ M : ℝ, 0 < M → T_hawking M = T_hawking_of_radius (2 * M)
 180  T_hawking_pos : ∀ M : ℝ, 0 < M → 0 < T_hawking M
 181  T_hawking_of_radius_pos :
 182    ∀ r_s : ℝ, 0 < r_s → 0 < T_hawking_of_radius r_s
 183  mass_lt_implies_temp_gt :
 184    ∀ M₁ M₂ : ℝ, 0 < M₁ → 0 < M₂ → M₁ < M₂ →
 185      T_hawking M₂ < T_hawking M₁
 186  t_Page_def : ∀ M : ℝ, t_Page M = 5120 * Real.pi * M ^ 3
 187  t_Page_pos : ∀ M : ℝ, 0 < M → 0 < t_Page M
 188  mass_lt_implies_page_lt :
 189    ∀ M₁ M₂ : ℝ, 0 < M₁ → 0 < M₂ → M₁ < M₂ → t_Page M₁ < t_Page M₂
 190  temp_times_page_eq_M_sq :
 191    ∀ M : ℝ, 0 < M → T_hawking M * t_Page M = 640 * M ^ 2
 192
 193def hawkingTemperatureCert : HawkingTemperatureCert where
 194  T_hawking_def := T_hawking_def
 195  T_hawking_of_radius_def := T_hawking_of_radius_def
 196  T_hawking_eq_radius_form := T_hawking_eq_radius_form
 197  T_hawking_pos := T_hawking_pos
 198  T_hawking_of_radius_pos := T_hawking_of_radius_pos
 199  mass_lt_implies_temp_gt := mass_lt_implies_temp_gt
 200  t_Page_def := t_Page_def
 201  t_Page_pos := t_Page_pos
 202  mass_lt_implies_page_lt := mass_lt_implies_page_lt
 203  temp_times_page_eq_M_sq := temp_times_page_eq_M_sq
 204
 205/-- **HAWKING TEMPERATURE ONE-STATEMENT.** In RS-native units, the
 206Hawking temperature of a Schwarzschild black hole is
 207`T_H(M) = 1/(8π M)`, equivalently `1/(4π r_s)` with `r_s = 2 M`.
 208The temperature is positive, strictly decreasing in `M` (lighter
 209holes are hotter), and the Page time scales as `M³` from the
 210standard `dM/dt = −1/(M²)` evaporation law. The product
 211`T_H · t_Page` scales as the horizon area (`M²`), recovering the
 212RS rung-counting structure of `BlackHoleEntropyFromLedger`. -/
 213theorem hawking_temperature_one_statement :
 214    (∀ M : ℝ, T_hawking M = 1 / (8 * Real.pi * M)) ∧
 215    (∀ M : ℝ, 0 < M → 0 < T_hawking M) ∧
 216    (∀ M₁ M₂ : ℝ, 0 < M₁ → 0 < M₂ → M₁ < M₂ →
 217        T_hawking M₂ < T_hawking M₁) ∧
 218    (∀ M : ℝ, 0 < M → T_hawking M * t_Page M = 640 * M ^ 2) :=
 219  ⟨T_hawking_def, T_hawking_pos, mass_lt_implies_temp_gt,
 220   temp_times_page_eq_M_sq⟩
 221
 222end
 223
 224end HawkingTemperatureFromRung
 225end Gravity
 226end IndisputableMonolith
 227