structure definition def or abbrev

`AdSCFT`

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

formal statement (Lean)

 174structure AdSCFT where
 175  /-- Dimension of the bulk. -/
 176  bulk_dim : ℕ
 177  /-- Dimension of the boundary. -/
 178  boundary_dim : ℕ
 179  /-- Boundary is one dimension lower. -/
 180  dim_relation : boundary_dim = bulk_dim - 1
 181
 182/-- **THEOREM (Ryu-Takayanagi Formula)**: Entanglement entropy in the CFT
 183    equals the area of the minimal surface in the bulk.
 184    S_EE = Area(γ_A) / (4G_N) -/

depends on (19)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Dimension in IndisputableMonolith.Constants.Dimensions decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
Dimension in IndisputableMonolith.Foundation.DimensionForcing decl_use
entropy in IndisputableMonolith.Foundation.InitialCondition decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
G_N in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use
entropy in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
entropy in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use