planckLength

formal source

  44/-! ## Fundamental Scales -/
  45
  46/-- The Planck length l_P = √(ℏG/c³) ≈ 1.6 × 10⁻³⁵ m. -/
  47noncomputable def planckLength : ℝ := Real.sqrt (hbar * G / c^3)
  48
  49/-- The Planck area l_P² ≈ 2.6 × 10⁻⁷⁰ m². -/
  50noncomputable def planckArea : ℝ := planckLength^2
  51
  52/-- The Planck mass m_P = √(ℏc/G) ≈ 2.2 × 10⁻⁸ kg. -/
  53noncomputable def planckMass : ℝ := Real.sqrt (hbar * c / G)
  54
  55/-- The Planck temperature T_P = √(ℏc⁵/(G k_B²)) ≈ 1.4 × 10³² K. -/
  56noncomputable def planckTemperature : ℝ := planckMass * c^2 / k_B
  57
  58/-! ## Black Hole Properties -/
  59
  60/-- A Schwarzschild black hole with mass M. -/
  61structure BlackHole where
  62  mass : ℝ
  63  mass_pos : mass > 0
  64
  65/-- The Schwarzschild radius r_s = 2GM/c². -/
  66noncomputable def schwarzschildRadius (bh : BlackHole) : ℝ :=
  67  2 * G * bh.mass / c^2
  68
  69/-- The horizon area A = 4π r_s². -/
  70noncomputable def horizonArea (bh : BlackHole) : ℝ :=
  71  4 * Real.pi * (schwarzschildRadius bh)^2
  72
  73/-! ## Bekenstein-Hawking Entropy -/
  74
  75/-- The Bekenstein-Hawking entropy S_BH = k_B A / (4 l_P²).
  76
  77    This is the maximum entropy that can fit in a region