structure
definition
FallingEntry
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Quantum.BlackHoleInformation on GitHub at line 106.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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