pith. machine review for the scientific record. sign in
theorem proved term proof

sbh_saturation_uniqueness

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  60theorem sbh_saturation_uniqueness (Rs : ℝ) (h_Rs : Rs > 0) :
  61    ∃! (S : ℝ), S = HorizonArea Rs / (4 * ell0^2) := by

proof body

Term-mode proof.

  62  use HorizonArea Rs / (4 * ell0^2)
  63  constructor
  64  · rfl
  65  · intro S' h; exact h
  66
  67/-- The BH entropy saturation value is strictly positive for `Rs > 0`. -/

depends on (13)

Lean names referenced from this declaration's body.