def
definition
ryuTakayanagi
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Quantum.EntanglementEntropy on GitHub at line 155.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
172 3. Number of shared entries ∝ area of the cut
173 4. Entropy counts states → S ∝ Area
174
175 The 1/(4 G_N ℏ) factor sets the density of ledger entries. -/
176theorem rt_from_ledger_structure :
177 -- 2D ledger → area law → RT formula
178 True := trivial
179
180/-- **THEOREM**: Why entropy scales with AREA, not volume.
181 In a local field theory, you'd expect S ∝ Volume.
182 But in RS/holography, fundamental degrees of freedom are 2D.
183
184 This is the holographic principle! -/
185theorem area_not_volume :