  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):
  73      S_rad = S_0 × f  (grows linearly)
  74
  75    After Page time (f > 1/2):
  76      S_rad = S_0 × (1 - f)  (decreases linearly)
  77
  78    This forms the "Page curve" - a tent-shaped function. -/
  79noncomputable def pageEntropy (bh : EvolvingBlackHole) : ℝ :=
  80  if bh.evaporation_fraction ≤ pageTime then
  81    radiationEntropyNaive bh
  82  else
  83    remainingEntropy bh
  84
  85/-- **THEOREM**: Page entropy is maximized at f = 1/2. -/
  86theorem page_entropy_max_at_half (S₀ : ℝ) (hS : S₀ > 0) :
  87    -- The maximum S_rad = S_0/2 occurs at f = 1/2

papers checked against this theorem

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