`k_B`

definition

show as: view math explainer →

module: IndisputableMonolith.Quantum.PageCurve
domain: Quantum
line: 42 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Quantum.PageCurve on GitHub at line 42.

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

  39open IndisputableMonolith.Cost
  40
  41/-- Boltzmann constant. -/
  42noncomputable def k_B : ℝ := 1.380649e-23
  43
  44/-! ## The Page Curve Setup -/
  45
  46/-- A black hole with evolving entropy. -/
  47structure EvolvingBlackHole where
  48  /-- Initial Bekenstein-Hawking entropy (in bits) -/
  49  S_initial : ℝ
  50  /-- Fraction of initial mass that has evaporated (0 to 1) -/
  51  evaporation_fraction : ℝ
  52  /-- Validity constraints -/
  53  s_pos : S_initial > 0
  54  frac_valid : 0 ≤ evaporation_fraction ∧ evaporation_fraction ≤ 1
  55
  56/-- The remaining black hole entropy. -/
  57noncomputable def remainingEntropy (bh : EvolvingBlackHole) : ℝ :=
  58  bh.S_initial * (1 - bh.evaporation_fraction)
  59
  60/-- The entropy carried away by radiation (naive, before Page time). -/
  61noncomputable def radiationEntropyNaive (bh : EvolvingBlackHole) : ℝ :=
  62  bh.S_initial * bh.evaporation_fraction
  63
  64/-! ## The Page Curve -/
  65
  66/-- The Page time: when half the initial entropy has been radiated.
  67    This occurs at evaporation_fraction = 1/2. -/
  68noncomputable def pageTime : ℝ := 1 / 2
  69
  70/-- The entanglement entropy of the radiation (the Page curve).
  71
  72    Before Page time (f < 1/2):

papers checked against this theorem

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