def
definition
G_N
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Quantum.EntanglementEntropy on GitHub at line 51.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
48/-! ## Fundamental Constants -/
49
50/-- Newton's gravitational constant (SI units). -/
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