informationCapacity

formal source

  88/-! ## Information Content -/
  89
  90/-- Number of bits that can be stored in a black hole (from entropy). -/
  91noncomputable def informationCapacity (bh : BlackHole) : ℝ :=
  92  bekensteinHawkingEntropy bh / Real.log 2
  93
  94/-- The holographic bound: information ≤ A/4 bits. -/
  95noncomputable def holographicBound (area : ℝ) : ℝ := area / (4 * Real.log 2)
  96
  97/-- **THEOREM**: Black hole saturates the holographic bound. -/
  98theorem bh_saturates_holographic (bh : BlackHole) :
  99    informationCapacity bh = holographicBound (horizonArea bh) := by
 100  unfold informationCapacity holographicBound bekensteinHawkingEntropy
 101  ring
 102
 103/-! ## Ledger Model of Black Holes -/
 104
 105/-- A ledger entry that falls into a black hole. -/
 106structure FallingEntry where
 107  /-- The original information content. -/
 108  information : ℕ  -- bits
 109  /-- Time of infall. -/
 110  infallTime : ℝ
 111  /-- The entry is not destroyed, just compressed. -/
 112  preserved : True
 113
 114/-- The black hole ledger: compressed entries on the horizon. -/
 115structure BlackHoleLedger where
 116  /-- Entries that have fallen in. -/
 117  entries : List FallingEntry
 118  /-- Total information content. -/
 119  totalInfo : ℕ
 120  /-- Consistency: total = sum of parts. -/
 121  consistent : totalInfo = (entries.map FallingEntry.information).sum