pith. machine review for the scientific record. sign in
structure definition def or abbrev

HorizonLedger

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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. -/

depends on (10)

Lean names referenced from this declaration's body.