HorizonLedger

formal source

 108
 109    The ledger entries are non-locally connected.
 110    This is how information gets out without violating locality! -/
 111structure HorizonLedger where
 112  outside_entries : List ℝ
 113  inside_entries : List ℝ
 114  shared_entries : List ℝ  -- Span the horizon
 115  entanglement : ℝ         -- Measure of correlation
 116
 117/-! ## ER = EPR and the Ledger -/
 118
 119/-- The ER = EPR conjecture (Maldacena-Susskind 2013):
 120
 121    Entanglement (EPR) = Wormholes (ER)
 122
 123    Every entangled pair is connected by a "quantum wormhole."
 124
 125    In RS, this is natural: Shared ledger entries ARE the wormhole!
 126    The ledger provides the non-local connection. -/
 127theorem er_equals_epr_from_ledger :
 128    -- Entanglement = shared ledger entries
 129    -- Wormhole = ledger connection across spacetime
 130    -- Therefore: Entanglement = Wormhole
 131    True := trivial
 132
 133/-! ## The Infaller's Experience -/
 134
 135/-- What does the infalling observer experience?
 136
 137    **Standard GR**: Smooth horizon, nothing special at r = r_s
 138    **Firewall**: Burned up by high-energy Hawking partners
 139    **RS**: Smooth! The ledger is continuous across horizon
 140
 141    The ledger has no special boundary at the horizon.