planckArea

formal source

  57noncomputable def planckLength : ℝ := Real.sqrt (hbar * G_N / (c^3))
  58
  59/-- The Planck area. -/
  60noncomputable def planckArea : ℝ := planckLength^2
  61
  62/-! ## The Bekenstein-Hawking Entropy -/
  63
  64/-- The Bekenstein-Hawking entropy of a black hole.
  65    S_BH = A / (4 × l_p²) = A / (4 G_N ℏ / c³) -/
  66noncomputable def bekensteinHawkingEntropy (area : ℝ) : ℝ :=
  67  area * c^3 / (4 * G_N * hbar)
  68
  69/-- **THEOREM**: BH entropy is proportional to area. -/
  70theorem bh_entropy_proportional_to_area (a1 a2 : ℝ) (h : a2 = 2 * a1) :
  71    bekensteinHawkingEntropy a2 = 2 * bekensteinHawkingEntropy a1 := by
  72  unfold bekensteinHawkingEntropy
  73  rw [h]
  74  ring
  75
  76/-- **THEOREM**: BH entropy is positive for positive area. -/
  77theorem bh_entropy_positive (area : ℝ) (h : area > 0) :
  78    bekensteinHawkingEntropy area > 0 := by
  79  unfold bekensteinHawkingEntropy G_N hbar
  80  -- area * c^3 / (4 * G_N * hbar) > 0
  81  -- All factors are positive
  82  have hc : c > 0 := c_pos
  83  have hc3 : c^3 > 0 := pow_pos hc 3
  84  have hG : (6.674e-11 : ℝ) > 0 := by norm_num
  85  have hh : (1.054e-34 : ℝ) > 0 := by norm_num
  86  have hdenom : 4 * (6.674e-11 : ℝ) * (1.054e-34 : ℝ) > 0 := by positivity
  87  apply div_pos
  88  · exact mul_pos h hc3
  89  · exact hdenom
  90