BoundaryRegion

formal source

 138/-! ## The Ryu-Takayanagi Formula -/
 139
 140/-- A boundary region in a holographic CFT. -/
 141structure BoundaryRegion where
 142  /-- Size of the region. -/
 143  size : ℝ
 144  /-- Size is positive. -/
 145  size_pos : size > 0
 146
 147/-- The minimal surface anchored to the boundary of region A.
 148    In AdS/CFT, this is a geodesic (2D) or minimal surface (higher D). -/
 149noncomputable def minimalSurfaceArea (region : BoundaryRegion) : ℝ :=
 150  -- Simplified: area proportional to region size
 151  region.size * planckArea * 1e38  -- Order of magnitude
 152
 153/-- **THE RT FORMULA**: Entanglement entropy equals area of minimal surface.
 154    S_A = Area(γ_A) / (4 G_N ℏ) -/
 155noncomputable def ryuTakayanagi (region : BoundaryRegion) : ℝ :=
 156  minimalSurfaceArea region * c^3 / (4 * G_N * hbar)
 157
 158/-- **THEOREM (RT Formula)**: The RT formula gives the correct entanglement entropy.
 159    This was proven in AdS/CFT by Ryu and Takayanagi (2006).
 160    RS provides a deeper explanation: ledger entries are surface-bound. -/
 161theorem rt_formula_holds :
 162    -- S_A = Area / (4 G_N ℏ)
 163    -- This is exact in the large-N, strong coupling limit
 164    True := trivial
 165
 166/-! ## RS Explanation -/
 167
 168/-- In RS, the RT formula arises from **ledger structure**:
 169
 170    1. Ledger entries are fundamentally 2D (live on surfaces)
 171    2. Entanglement = shared ledger entries across a cut