`hbar`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Quantum.EntanglementEntropy on GitHub at line 54.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.