structure
definition
def or abbrev
LedgerEvolution
show as:
view Lean formalization →
formal statement (Lean)
116structure LedgerEvolution where
117 bh_entries : ℝ -- Ledger entries in BH
118 rad_entries : ℝ -- Ledger entries in radiation
119 entanglement : ℝ -- Shared entanglement
120 conservation : bh_entries + rad_entries = total_entries
121 total_entries : ℝ
122
123/-! ## The Information Paradox Resolution -/
124
125/-- The information paradox: Does information survive black hole evaporation?
126
127 **Hawking's calculation**: Radiation is thermal → information lost
128 **Page's insight**: If unitary, entropy must follow Page curve
129 **RS resolution**: Ledger conservation ensures unitarity -/