def definition def or abbrev

`ryuTakayanagi`

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

formal statement (Lean)

 155noncomputable def ryuTakayanagi (region : BoundaryRegion) : ℝ :=

proof body

Definition body.

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

depends on (12)

Lean names referenced from this declaration's body.

hbar in IndisputableMonolith.Constants decl_use
hbar in IndisputableMonolith.Constants.Codata decl_use
entropy in IndisputableMonolith.Foundation.InitialCondition decl_use
was in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
hbar in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
BoundaryRegion in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
G_N in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
hbar in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
minimalSurfaceArea in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
entropy in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
entropy in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use