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)
149noncomputable def minimalSurfaceArea (region : BoundaryRegion) : ℝ :=
proof body
Definition body.
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 ℏ) -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
ryuTakayanagi
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
depends on (13)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
entropy
in IndisputableMonolith.Foundation.InitialCondition
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
planckArea
in IndisputableMonolith.Quantum.BekensteinHawking
decl_use
-
BoundaryRegion
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
G_N
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
planckArea
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
planckArea
in IndisputableMonolith.Quantum.HolographicBound
decl_use
-
entropy
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
entropy
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use