addEntry

formal source

 121  consistent : totalInfo = (entries.map FallingEntry.information).sum
 122
 123/-- Add an entry to the black hole ledger. -/
 124def addEntry (ledger : BlackHoleLedger) (entry : FallingEntry) : BlackHoleLedger :=
 125  ⟨entry :: ledger.entries,
 126   ledger.totalInfo + entry.information,
 127   by simp only [List.map_cons, List.sum_cons]; rw [ledger.consistent]; ring⟩
 128
 129/-- **THEOREM**: Information is preserved when falling into a black hole. -/
 130theorem information_preserved_on_infall (ledger : BlackHoleLedger) (entry : FallingEntry) :
 131    (addEntry ledger entry).totalInfo = ledger.totalInfo + entry.information := rfl
 132
 133/-! ## Hawking Radiation and Information Return -/
 134
 135/-- A Hawking radiation quantum carrying information. -/
 136structure HawkingQuantum where
 137  /-- Energy of the quantum. -/
 138  energy : ℝ
 139  /-- Information carried (in correlations). -/
 140  informationBits : ℕ
 141  /-- The quantum is entangled with interior. -/
 142  entangled : True
 143
 144/-- The evaporation process: black hole → radiation. -/
 145structure EvaporationProcess where
 146  /-- Initial black hole. -/
 147  initialBH : BlackHole
 148  /-- Emitted Hawking quanta. -/
 149  radiation : List HawkingQuantum
 150  /-- Total information in radiation. -/
 151  radiatedInfo : ℕ
 152  /-- Remaining black hole mass (can go to zero). -/
 153  remainingMass : ℝ
 154