`hbar`

definition

show as: view math explainer →

module: IndisputableMonolith.Quantum.EntanglementEntropy
domain: Quantum
line: 54 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Quantum.EntanglementEntropy on GitHub at line 54.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  51noncomputable def G_N : ℝ := 6.674e-11
  52
  53/-- Planck's reduced constant (SI units). -/
  54noncomputable def hbar : ℝ := 1.054e-34
  55
  56/-- The Planck length. -/
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.