structure definition def or abbrev

`BoundaryRegion`

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

formal statement (Lean)

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

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

minimalSurfaceArea in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
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
or in IndisputableMonolith.Constants.EulerMascheroni decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived 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
A in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
A in IndisputableMonolith.Modal.Actualization decl_use