diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean
index 71341f2fe..e80b3f031 100644
--- a/PhyslibAlpha.lean
+++ b/PhyslibAlpha.lean
@@ -39,3 +39,14 @@ public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.Invariants
 public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.Module
 public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.OrbitRepresentative
 public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.SwapDoublet
+public import PhyslibAlpha.StringTheory.DBranes.Basic
+public import PhyslibAlpha.StringTheory.DBranes.CoulombBranch.Complexity
+public import PhyslibAlpha.StringTheory.DBranes.CoulombBranch.Shell
+public import PhyslibAlpha.StringTheory.DBranes.CoulombBranch.SphereEntanglement
+public import PhyslibAlpha.StringTheory.DBranes.CoulombBranch.StripEntanglement
+public import PhyslibAlpha.StringTheory.DBranes.CoulombBranch.TargetSpaceEntanglement
+public import PhyslibAlpha.StringTheory.DBranes.DecouplingLimit
+public import PhyslibAlpha.StringTheory.Holography.Complexity
+public import PhyslibAlpha.StringTheory.Holography.EntropicCFunction
+public import PhyslibAlpha.StringTheory.Holography.FlatSpaceRT
+public import PhyslibAlpha.StringTheory.Holography.RyuTakayanagi
diff --git a/PhyslibAlpha/StringTheory/DBranes/Basic.lean b/PhyslibAlpha/StringTheory/DBranes/Basic.lean
new file mode 100644
index 000000000..eb4163d8d
--- /dev/null
+++ b/PhyslibAlpha/StringTheory/DBranes/Basic.lean
@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import Physlib.Meta.Informal.Basic
+/-!
+# Dp-brane supergravity backgrounds
+
+## i. Overview
+
+Dp-branes are `(p+1)`-dimensional extended objects of type II string theory which carry tension
+and Ramond-Ramond charge. At low energies, a stack of `N` coincident Dp-branes sources a
+classical solution of type II supergravity — an extremal black `p`-brane — which is determined
+entirely by a single function `H`, harmonic on the `(9-p)`-dimensional space transverse to the
+branes. In the Einstein frame the background is
+
+`ds²_E = H^((p-7)/8) (-dt² + dx²_∥) + H^((p+1)/8) (dr² + r² dΩ²_{8-p})`,
+
+`e^φ = g_s H^((3-p)/4)`,
+
+together with `N` units of Ramond-Ramond flux through the transverse sphere. For branes
+stacked at the origin the harmonic function is `H(r) = 1 + (r_p/r)^(7-p)`, where the scale
+`r_p` is set by `g_s N` in string units.
+
+The linearity of Laplace's equation makes this family of backgrounds highly reusable: *any*
+distribution of branes in the transverse space yields a solution, with `H` the corresponding
+electrostatic potential. Multi-center solutions, continuous distributions, and the spherical
+shells of `PhyslibAlpha.StringTheory.DBranes.CoulombBranch.Shell` all arise this way. The
+near-horizon limit of the stacked solution, and the gauge/gravity duality it supports, are
+developed in `PhyslibAlpha.StringTheory.DBranes.DecouplingLimit`.
+
+## ii. Key results
+
+- `DBrane.dpBraneScale` : the length scale `r_p` of the background sourced by `N` Dp-branes.
+- `DBrane.dpBraneHarmonicFunction` : the harmonic function `H(r) = 1 + (r_p/r)^(7-p)` of a
+  stack of branes at the origin.
+- `DBrane.dpBraneMetric` : the Einstein-frame metric determined by a transverse-harmonic
+  function.
+- `DBrane.dpBraneDilaton` : the corresponding dilaton profile.
+- `DBrane.dpBraneMetric_solves_supergravity` : these backgrounds solve the type II
+  supergravity equations of motion.
+
+## iii. Table of contents
+
+- A. The brane scale and harmonic function
+- B. The background fields
+- C. The supergravity equations
+
+## iv. References
+
+- G. T. Horowitz and A. Strominger, *Black strings and p-branes*, Nucl. Phys. B360 (1991) 197.
+- K. S. Stelle, *BPS branes in supergravity*, arXiv:hep-th/9803116.
+- E. Jørstad, R. C. Myers and S. Pasterski, *Flat Space Entanglement: A Coulomb Branch
+  Perspective*, arXiv:2606.13889, section 2.2.
+
+-/
+
+@[expose] public section
+
+namespace DBrane
+
+/-!
+
+## A. The brane scale and harmonic function
+
+-/
+
+/-- The length scale `r_p` of the supergravity background sourced by a stack of `N` coincident
+Dp-branes, determined by
+
+`r_p^(7-p) = 2^(5-p) π^((5-p)/2) Γ((7-p)/2) g_s N ℓ_s^(7-p)`
+
+where `g_s` is the string coupling and `ℓ_s` the string length. This is the scale at which the
+harmonic function of the stacked-brane background transitions between its asymptotically flat
+and near-horizon behaviors; it is the gravitational analogue of the charge radius of the
+stack. -/
+informal_definition dpBraneScale where
+  deps := []
+  tag := "GF3NV"
+
+/-- The harmonic function of the background sourced by `N` coincident Dp-branes at the origin
+of the transverse space:
+
+`H(r) = 1 + (r_p/r)^(7-p)`
+
+where `r` is the radial coordinate in the `(9-p)`-dimensional transverse space and `r_p` is
+`DBrane.dpBraneScale`. It is harmonic away from the origin, where the branes sit as a
+delta-function source, and tends to `1` at infinity, where the background becomes flat
+ten-dimensional Minkowski space. More general brane distributions are described by the
+harmonic function equal to the electrostatic potential of the corresponding charge
+distribution. -/
+informal_definition dpBraneHarmonicFunction where
+  deps := [``dpBraneScale]
+  tag := "GF3NX"
+
+/-!
+
+## B. The background fields
+
+-/
+
+/-- The Einstein-frame metric of the background sourced by Dp-branes with transverse-harmonic
+function `H`:
+
+`ds²_E = H^((p-7)/8) (-dt² + dx²_∥) + H^((p+1)/8) (dr² + r² dΩ²_{8-p})`
+
+where `x_∥` are the `p` spatial worldvolume directions and `dΩ²_{8-p}` is the round metric on
+the unit `(8-p)`-sphere of the transverse space. For a stack of `N` branes at the origin, `H`
+is `DBrane.dpBraneHarmonicFunction`; any other transverse-harmonic `H` gives the metric of the
+corresponding brane distribution. -/
+informal_definition dpBraneMetric where
+  deps := [``dpBraneHarmonicFunction]
+  tag := "GF3NZ"
+
+/-- The dilaton profile of a Dp-brane background with transverse-harmonic function `H`:
+
+`e^φ = g_s H^((3-p)/4)`.
+
+For `p < 3` the dilaton grows where `H` grows (near the branes), for `p > 3` it decreases
+there, and for `p = 3` it is constant — the special feature of D3-branes underlying the
+conformal invariance of their worldvolume theory. -/
+informal_definition dpBraneDilaton where
+  deps := [``dpBraneHarmonicFunction]
+  tag := "GF3N3"
+
+/-!
+
+## C. The supergravity equations
+
+-/
+
+/-- The Dp-brane background — the metric `DBrane.dpBraneMetric`, the dilaton
+`DBrane.dpBraneDilaton` and the Ramond-Ramond `(p+1)`-form potential `C_{01…p} ∝ H⁻¹` with `N`
+units of flux through the transverse sphere — solves the equations of motion of type II
+supergravity (type IIA for `p` even, type IIB for `p` odd) for *any* function `H` harmonic on
+the transverse space, with brane sources located where `H` fails to be harmonic. This
+linearity in the source distribution underlies multi-center and shell solutions. -/
+informal_lemma dpBraneMetric_solves_supergravity where
+  deps := [``dpBraneMetric, ``dpBraneDilaton]
+  tag := "GF3N5"
+
+end DBrane
+
+end
diff --git a/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/Complexity.lean b/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/Complexity.lean
new file mode 100644
index 000000000..86bdf46b5
--- /dev/null
+++ b/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/Complexity.lean
@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import PhyslibAlpha.StringTheory.DBranes.CoulombBranch.Shell
+public import PhyslibAlpha.StringTheory.Holography.Complexity
+/-!
+# Holographic complexity of shell geometries
+
+## i. Overview
+
+This module is built around the complexity-equals-volume complexity of a Coulomb-branch shell
+state, `DBrane.CoulombBranch.shellComplexityVolume`: the shell geometry is static, so the
+maximal bulk slice of the CV proposal is the constant-time slice, and the complexity is its
+regulated volume. The volume splits into a throat contribution from `R < r < r_uv`, identical
+to the throat vacuum, and a flat-bubble contribution from `r < R`.
+
+The bubble contributes less volume than the throat region it replaces, so the complexity of
+the Coulomb-branch state is reduced relative to the throat vacuum at the same cutoff, with a
+deficit growing with the shell radius. Complexity thus shows the same infrared depletion as
+the entanglement entropy of the shell state: by every holographic measure of degrees of
+freedom considered here, the flat-space bubble is poorer than the throat it replaces.
+
+## ii. Key results
+
+- `DBrane.CoulombBranch.shellComplexityVolume` : the CV complexity of the shell state.
+- `DBrane.CoulombBranch.shellComplexity_suppressed` : the complexity of the shell state is
+  reduced relative to the throat vacuum.
+
+## iii. Table of contents
+
+- A. The complexity of the shell state
+
+## iv. References
+
+- E. Jørstad, R. C. Myers and S. Pasterski, *Flat Space Entanglement: A Coulomb Branch
+  Perspective*, arXiv:2606.13889, section 5.
+- D. Stanford and L. Susskind, *Complexity and Shock Wave Geometries*, arXiv:1406.2678.
+
+-/
+
+@[expose] public section
+
+namespace DBrane
+
+namespace CoulombBranch
+
+/-!
+
+## A. The complexity of the shell state
+
+-/
+
+/-- The complexity-equals-volume complexity of the Coulomb-branch shell state: the volume of
+the constant-time slice of the shell geometry inside the cutoff surface `r = r_uv`, computed
+with the Einstein-frame metric and divided by `G_N` and the appropriate bulk length scale, as
+in `Holography.complexityVolume`. Since the shell geometry is static, the maximal slice is
+the constant-time slice, and the volume splits into a throat contribution from `R < r < r_uv`
+and a flat-bubble contribution from `r < R`. -/
+informal_definition shellComplexityVolume where
+  deps := [``shellMetric, ``Holography.complexityVolume]
+  tag := "GF3P4"
+
+/-- The holographic complexity of the Coulomb-branch shell state is reduced relative to the
+Dp-brane throat vacuum at the same cutoff: the flat-space bubble contributes less volume than
+the throat region it replaces, the deficit growing with the shell radius. Holographic
+complexity thus exhibits the same qualitative infrared depletion as the entanglement entropy
+of the shell state: the flat-space region carries fewer effective degrees of freedom than the
+throat. See section 5 of arXiv:2606.13889. -/
+informal_lemma shellComplexity_suppressed where
+  deps := [``shellComplexityVolume]
+  tag := "GF3P6"
+
+end CoulombBranch
+
+end DBrane
+
+end
diff --git a/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/Shell.lean b/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/Shell.lean
new file mode 100644
index 000000000..ecc23abe4
--- /dev/null
+++ b/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/Shell.lean
@@ -0,0 +1,188 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import PhyslibAlpha.StringTheory.DBranes.DecouplingLimit
+/-!
+# Coulomb-branch shell geometries
+
+## i. Overview
+
+Maximally supersymmetric Yang-Mills theory has a moduli space of vacua — the Coulomb branch —
+on which the adjoint scalars acquire expectation values, breaking `U(N)` to `U(1)^N`.
+Holographically, moving onto the Coulomb branch corresponds to separating the `N` Dp-branes
+in the transverse space. Distributing them uniformly on a sphere of radius `R` produces the
+*shell geometry*: by the linearity of the supergravity solution in the brane distribution,
+its harmonic function is the electrostatic potential of a uniformly charged spherical shell,
+
+`H(r) = (r_p/r)^(7-p)` for `r ≥ R`, and `H(r) = (r_p/R)^(7-p)` for `r ≤ R`.
+
+Outside the shell the background is exactly the Dp-brane throat; inside, `H` is constant and
+the geometry is a bubble of flat ten-dimensional Minkowski space with constant dilaton. The
+shell geometry therefore embeds a flat-space region in the infrared of a standard holographic
+background, with the ultraviolet dictionary of the throat left untouched. This makes it a
+controlled, top-down setting for questions about flat-space holography: any boundary
+observable that probes deep enough in the infrared becomes a probe of flat space.
+
+The scales of the geometry are as follows. The proper size of the shell is
+`R_shell ∝ r_p^((7-p)(p+1)/16) R^((p-3)²/16)`; for `p ≠ 3` it is adjustable through the
+modulus `R`, while for `p = 3` it is frozen at the AdS scale, a reflection of the conformal
+invariance of `𝒩 = 4` super Yang-Mills. Entanglement entropy, target space entanglement and
+holographic complexity in these backgrounds are developed in the sibling modules
+`StripEntanglement`, `SphereEntanglement`, `TargetSpaceEntanglement` and `Complexity`.
+
+## ii. Key results
+
+- `DBrane.CoulombBranch.shellHarmonicFunction` : the piecewise harmonic function of a
+  spherical shell of Dp-branes.
+- `DBrane.CoulombBranch.shellMetric` : the corresponding shell geometry.
+- `DBrane.CoulombBranch.shellMetric_interior_flat` : the interior of the shell is a bubble of
+  flat Minkowski space.
+- `DBrane.CoulombBranch.shellMetric_solves_supergravity` : the shell geometry solves the
+  supergravity equations with a brane source on the shell.
+- `DBrane.CoulombBranch.CoulombBranchVacuum` : the dual description as a Coulomb-branch
+  vacuum of maximally supersymmetric Yang-Mills theory.
+- `DBrane.CoulombBranch.properShellRadius` : the proper size of the shell.
+- `DBrane.CoulombBranch.properShellRadius_p3_fixed` : for `p = 3` the proper shell size is
+  independent of the shell radius `R`.
+- `DBrane.CoulombBranch.uvCutoffOfRadialCutoff` : the map between the bulk radial cutoff and
+  the gauge theory UV cutoff.
+
+## iii. Table of contents
+
+- A. The shell geometry
+- B. The flat-space bubble
+- C. The dual Coulomb-branch vacuum
+- D. Scales of the shell geometry
+
+## iv. References
+
+- P. Kraus, F. Larsen and S. P. Trivedi, *The Coulomb branch of gauge theory from rotating
+  branes*, arXiv:hep-th/9811120.
+- E. Jørstad, R. C. Myers and S. Pasterski, *Flat Space Entanglement: A Coulomb Branch
+  Perspective*, arXiv:2606.13889, section 2.2.
+
+-/
+
+@[expose] public section
+
+namespace DBrane
+
+namespace CoulombBranch
+
+/-!
+
+## A. The shell geometry
+
+-/
+
+/-- The harmonic function of `N` Dp-branes distributed uniformly on a sphere of radius `R` in
+the transverse space, in the decoupling limit:
+
+`H(r) = (r_p/r)^(7-p)` for `r ≥ R`, and `H(r) = (r_p/R)^(7-p)` for `r ≤ R`.
+
+This is the electrostatic potential of a uniformly charged spherical shell: it agrees with
+the throat harmonic function outside the shell and is constant inside. It is continuous but
+not differentiable at `r = R`, where the brane source is located. -/
+informal_definition shellHarmonicFunction where
+  deps := [``DBrane.dpBraneHarmonicFunction, ``DBrane.dpBraneScale]
+  tag := "GF3OF"
+
+/-- The shell geometry: the Dp-brane background (Einstein-frame metric, dilaton and
+Ramond-Ramond flux) built from the piecewise harmonic function
+`DBrane.CoulombBranch.shellHarmonicFunction`. For `r > R` it coincides with the Dp-brane
+throat `DBrane.dpBraneThroatMetric`; for `r < R` the harmonic function is constant and the
+geometry is flat. -/
+informal_definition shellMetric where
+  deps := [``shellHarmonicFunction, ``DBrane.dpBraneMetric, ``DBrane.dpBraneDilaton]
+  tag := "GF3OH"
+
+/-- The shell geometry solves the equations of motion of type II supergravity everywhere away
+from the shell `r = R`, and across the shell the discontinuity in the derivative of the
+harmonic function is accounted for by the stress tensor and charge of the `N` Dp-branes
+distributed on the shell. In particular the Israel junction conditions at `r = R` are
+satisfied by the brane source. -/
+informal_lemma shellMetric_solves_supergravity where
+  deps := [``shellMetric, ``DBrane.dpBraneMetric_solves_supergravity]
+  tag := "GF3OK"
+
+/-!
+
+## B. The flat-space bubble
+
+-/
+
+/-- The interior region `r < R` of the shell geometry is isometric to a region of flat
+ten-dimensional Minkowski space, with constant dilaton. The constant value
+`H = (r_p/R)^(7-p)` of the harmonic function inside the shell rescales the worldvolume and
+transverse coordinates but produces no curvature. The shell geometry thus contains a bubble
+of flat space in its infrared region, glued to the Dp-brane throat across the shell. -/
+informal_lemma shellMetric_interior_flat where
+  deps := [``shellMetric]
+  tag := "GF3OI"
+
+/-!
+
+## C. The dual Coulomb-branch vacuum
+
+-/
+
+/-- The state of `(p+1)`-dimensional maximally supersymmetric `U(N)` Yang-Mills theory dual
+to the shell geometry: a vacuum on the Coulomb branch in which the expectation values of the
+adjoint scalars break `U(N)` to `U(1)^N`, with the `N` eigenvalue vectors distributed
+uniformly on a sphere in the `(9-p)`-dimensional moduli space whose radius corresponds to the
+shell radius `R` under the holographic dictionary. The W-bosons connecting the branes have
+masses set by the shell radius, and the deep infrared physics is that of the surviving
+`U(1)^N` degrees of freedom. -/
+informal_definition CoulombBranchVacuum where
+  deps := [``shellMetric]
+  tag := "GF3OM"
+
+/-!
+
+## D. Scales of the shell geometry
+
+-/
+
+/-- The proper size of the shell in the shell geometry: the proper radius of the transverse
+sphere `r = R` measured with the Einstein-frame metric,
+
+`R_shell = r_p^((7-p)(p+1)/16) R^((p-3)²/16)`
+
+up to a numerical constant. See section 2.2 of arXiv:2606.13889. -/
+informal_definition properShellRadius where
+  deps := [``shellMetric]
+  tag := "GF3OO"
+
+/-- For `p = 3` the proper shell radius `DBrane.CoulombBranch.properShellRadius` is
+independent of the shell radius `R`, being fixed at the AdS scale `r_3`: the exponent
+`(p-3)²/16` vanishes. This reflects the conformal invariance of four-dimensional `𝒩 = 4`
+super Yang-Mills, for which the modulus `R` is a flat direction changing no proper scale of
+the geometry. For `p ≠ 3` the proper shell size is instead a genuinely adjustable modulus,
+which controls the competition between extremal surfaces in holographic entanglement
+calculations. -/
+informal_lemma properShellRadius_p3_fixed where
+  deps := [``properShellRadius]
+  tag := "GF3OQ"
+
+/-- The relation between the bulk radial cutoff `r = r_uv` of the shell (or throat) geometry
+and the short-distance cutoff `δ` of the dual gauge theory: `δ` is the proper length in the
+gauge theory directions corresponding to the bulk cutoff surface, scaling as
+
+`δ ∝ (r_p/r_uv)^((5-p)/2) r_p`
+
+so that `r_uv → ∞` corresponds to `δ → 0` for `p < 5`. This map is used to express the UV
+divergences of holographic entanglement entropies in gauge theory terms. See section 2.2 of
+arXiv:2606.13889. -/
+informal_definition uvCutoffOfRadialCutoff where
+  deps := [``shellMetric]
+  tag := "GF3OS"
+
+end CoulombBranch
+
+end DBrane
+
+end
diff --git a/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/SphereEntanglement.lean b/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/SphereEntanglement.lean
new file mode 100644
index 000000000..0ae2996c7
--- /dev/null
+++ b/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/SphereEntanglement.lean
@@ -0,0 +1,191 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import PhyslibAlpha.StringTheory.DBranes.CoulombBranch.Shell
+public import PhyslibAlpha.StringTheory.Holography.RyuTakayanagi
+/-!
+# Spherical entanglement entropy in shell geometries
+
+## i. Overview
+
+This module is built around the area functional for RT surfaces anchored on a ball-shaped
+boundary region — bounded by a `(p-1)`-sphere of radius `P` in the gauge theory directions —
+in a Coulomb-branch shell geometry, `DBrane.CoulombBranch.sphereAreaFunctional`; its other
+declarations are properties of the extremal surfaces of this functional.
+
+Unlike the strip, the spherical problem has no conserved momentum and is not integrable: the
+extremal surfaces satisfy a nonlinear second-order differential equation for a curve
+`(r(σ), ρ(σ))` relating the bulk radial coordinate to the boundary radius. Surfaces are
+classified by how they close off — in the throat, inside the flat bubble, along an exact cone
+through the origin, or through the degenerate transverse sphere at `r = 0` at finite boundary
+radius. The cone
+
+`r ∝ (R/r_p)^((7-p)/2) ρ`
+
+is an exact extremal surface of the flat-region functional and governs the asymptotic shape
+of surfaces probing the deep interior of the bubble.
+
+For the conformal case `p = 3` the throat is `AdS₅ × S⁵` and small boundary spheres have the
+familiar hemispherical RT surfaces of anti-de Sitter space, closing off at `r_a = L²/P`. As
+`P` grows the RT surface descends into the flat bubble; in contrast with the strip, this
+happens as a smooth crossover rather than a first-order transition, the minimal surface
+deforming continuously through the closure classes. The growth of the regulated entropy with
+`P` is suppressed once the surface enters the bubble, so the spherical entangling surface
+sees the same infrared depletion of degrees of freedom as the strip, without the sharp
+transition.
+
+## ii. Key results
+
+- `DBrane.CoulombBranch.sphereAreaFunctional` : the piecewise area functional for spherical
+  surfaces in the shell geometry.
+- `DBrane.CoulombBranch.SphereClosureClasses` : the four ways candidate surfaces close off.
+- `DBrane.CoulombBranch.coneSurface`, `DBrane.CoulombBranch.coneSurface_extremal` : the exact
+  cone solution inside the flat bubble.
+- `DBrane.CoulombBranch.adsHemisphere_is_rt_surface` : for `p = 3` and small `P`, the RT
+  surfaces are the AdS₅ hemispheres.
+- `DBrane.CoulombBranch.sphereEntropy_transition_continuous` : the crossover to flat-space
+  probing surfaces is continuous.
+- `DBrane.CoulombBranch.sphereEntropy_large_radius_expansion` : the perturbative expansion of
+  the entropy at large `P`.
+
+## iii. Table of contents
+
+- A. The area functional for spherical surfaces
+- B. Closure classes and the cone solution
+- C. The conformal case
+- D. The crossover to the flat bubble
+
+## iv. References
+
+- E. Jørstad, R. C. Myers and S. Pasterski, *Flat Space Entanglement: A Coulomb Branch
+  Perspective*, arXiv:2606.13889, section 3.2 and appendices A, B.
+
+-/
+
+@[expose] public section
+
+namespace DBrane
+
+namespace CoulombBranch
+
+/-!
+
+## A. The area functional for spherical surfaces
+
+-/
+
+/-- The area functional for rotationally invariant surfaces in the shell geometry anchored on
+a `(p-1)`-sphere of radius `P` in the gauge theory directions, described by a curve
+`(r(σ), ρ(σ))` in the plane of the bulk radial coordinate `r` and the boundary radial
+coordinate `ρ`. It is the sum of a throat piece, of the schematic form
+
+`A_throat = Ω_{8-p} Ω_{p-1} r_p^(7-p) ∫ dσ r ρ^(p-1) √(r'² + (r/r_p)^(7-p) ρ'²)`,
+
+and a flat piece for the part of the surface at `r < R`, with the harmonic function frozen at
+its shell value. Extremal curves satisfy a nonlinear second-order ODE, matched across the
+shell by continuity of the curve and its first derivative. See section 3.2 of
+arXiv:2606.13889 for the precise expressions. -/
+informal_definition sphereAreaFunctional where
+  deps := [``shellMetric, ``Holography.BoundaryRegion]
+  tag := "GF3PF"
+
+/-!
+
+## B. Closure classes and the cone solution
+
+-/
+
+/-- The four ways a candidate extremal surface anchored on the `(p-1)`-sphere can close off
+in the shell geometry:
+
+- *throat closure*: the boundary sphere shrinks to a point, `ρ = 0`, at a radius `r_a > R` in
+  the throat;
+- *flat closure*: the boundary sphere shrinks to a point at a radius `0 < r_b < R` inside the
+  bubble;
+- *cone*: the surface approaches the origin `r = 0` and `ρ = 0` simultaneously along the
+  cone of `DBrane.CoulombBranch.coneSurface`;
+- *interior extension*: the surface reaches `r = 0` at a nonzero boundary radius `ρ_0 > 0`,
+  closing through the degenerate transverse sphere.
+
+The boundary conditions appropriate to each class, needed for the numerical integration of
+the extremal surface ODE, are detailed in appendix A of arXiv:2606.13889. -/
+informal_definition SphereClosureClasses where
+  deps := [``sphereAreaFunctional]
+  tag := "GF3PH"
+
+/-- The cone surface inside the flat bubble: the surface on which the bulk radial coordinate
+is proportional to the boundary radial coordinate,
+
+`r = √((8-p)/(p-1)) (R/r_p)^((7-p)/2) ρ`,
+
+passing through the origin `r = 0`, `ρ = 0` of the flat region. See section 3.2 of
+arXiv:2606.13889. -/
+informal_definition coneSurface where
+  deps := [``sphereAreaFunctional, ``shellMetric_interior_flat]
+  tag := "GF3PJ"
+
+/-- The cone surface `DBrane.CoulombBranch.coneSurface` is an exact extremal surface of the
+flat-region area functional: the powers of `r` and `ρ` in the area element balance precisely
+on the cone, so the nonlinear extremal surface equation is solved exactly. It plays the role
+for the sphere that the flat-sheeted surfaces play for the strip, governing the asymptotic
+shape of surfaces which probe the deep interior of the bubble. -/
+informal_lemma coneSurface_extremal where
+  deps := [``coneSurface]
+  tag := "GF3PL"
+
+/-!
+
+## C. The conformal case
+
+-/
+
+/-- For `p = 3`, where the throat is AdS₅ × S⁵ with AdS radius `L = r_3`, the extremal
+surfaces anchored on a sphere of radius `P` which close in the throat are the hemispheres
+
+`ρ(r) = √(P² - L⁴/r²)`,
+
+closing off at `r_a = L²/P`. These are the RT surfaces of the shell state whenever
+`r_a > R`, i.e. for boundary spheres of radius `P < L²/R`, and the entanglement entropy then
+agrees with the AdS₅ vacuum result. -/
+informal_lemma adsHemisphere_is_rt_surface where
+  deps := [``sphereAreaFunctional, ``SphereClosureClasses]
+  tag := "GF3PN"
+
+/-!
+
+## D. The crossover to the flat bubble
+
+-/
+
+/-- As the boundary sphere radius `P` increases, the RT surface of the shell geometry deforms
+continuously from throat-closing surfaces to surfaces probing the flat bubble: in contrast
+with the strip, there is no first-order exchange of dominance between disconnected families,
+the minimal surface instead passing smoothly through the closure classes of
+`DBrane.CoulombBranch.SphereClosureClasses`. The growth of the regulated entanglement entropy
+with `P` is suppressed once the surface enters the bubble, in qualitative agreement with the
+strip result `DBrane.CoulombBranch.stripEntropy_saturates`. See section 3.2 of
+arXiv:2606.13889, where this is established analytically for `p = 3` and numerically for
+`p = 2`. -/
+informal_lemma sphereEntropy_transition_continuous where
+  deps := [``SphereClosureClasses, ``adsHemisphere_is_rt_surface]
+  tag := "GF3PP"
+
+/-- For boundary spheres of large radius `P`, the entanglement entropy of the shell state
+admits a perturbative expansion around the limiting surface built from the cone
+`DBrane.CoulombBranch.coneSurface`, with corrections suppressed by inverse powers of `P`. The
+expansion confirms the suppression of the `P`-dependence of the regulated entropy found
+numerically. See appendix B of arXiv:2606.13889, where it is carried out for the `S²`
+entangling surface at `p = 3` and the `S¹` entangling surface at `p = 2`. -/
+informal_lemma sphereEntropy_large_radius_expansion where
+  deps := [``coneSurface_extremal, ``sphereEntropy_transition_continuous]
+  tag := "GF3PQ"
+
+end CoulombBranch
+
+end DBrane
+
+end
diff --git a/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/StripEntanglement.lean b/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/StripEntanglement.lean
new file mode 100644
index 000000000..805dff0d7
--- /dev/null
+++ b/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/StripEntanglement.lean
@@ -0,0 +1,221 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import PhyslibAlpha.StringTheory.DBranes.CoulombBranch.Shell
+public import PhyslibAlpha.StringTheory.Holography.EntropicCFunction
+/-!
+# Strip entanglement entropy in shell geometries
+
+## i. Overview
+
+This module is built around the area functional for strip-shaped RT surfaces in a
+Coulomb-branch shell geometry, `DBrane.CoulombBranch.stripAreaFunctional`; its other
+declarations are properties of the extremal surfaces of this functional and of the
+entanglement entropy they compute.
+
+Because the shell geometry consists of a Dp-brane throat glued to a flat bubble across the
+shell `r = R`, the variational problem for a strip of half-width `ℓ` is piecewise: surfaces
+extremize the throat area functional outside the shell and the flat-space one inside, and
+refract across the shell like light rays at an interface. The extremal surfaces fall into
+three classes — throat-confined, flat-bubble, and flat-sheeted — distinguished by how they
+close off, and the entanglement entropy is governed by the least-area class at each `ℓ`.
+
+The competition between the classes is resolved by a first-order transition at a critical
+width `ℓ_c ∝ (r_p/R)^((7-p)/2) R`, the boundary length scale dual to the shell radius. Narrow
+strips, `ℓ < ℓ_c`, have throat-confined RT surfaces and entanglement identical to the throat
+vacuum; wide strips, `ℓ > ℓ_c`, have flat-sheeted RT surfaces whose regulated area no longer
+depends on `ℓ`. The entropic c-function makes the physics of this saturation sharp: it runs
+with the throat vacuum value, of order `N²`, for `ℓ < ℓ_c` and vanishes identically for
+`ℓ > ℓ_c`. At scales where the boundary theory probes the flat-space bubble, it has only
+`O(1)` degrees of freedom in the large-`N` expansion — the flat infrared region of a
+Coulomb-branch vacuum is entanglement-depleted relative to the throat it replaces.
+
+## ii. Key results
+
+- `DBrane.CoulombBranch.stripAreaFunctional` : the piecewise area functional for strip
+  surfaces in the shell geometry.
+- `DBrane.CoulombBranch.stripRefractionCondition` : the matching of extremal surfaces across
+  the shell.
+- `DBrane.CoulombBranch.StripSurfaceClasses` : the three classes of candidate extremal
+  surfaces.
+- `DBrane.CoulombBranch.criticalStripWidth` : the critical half-width `ℓ_c`.
+- `DBrane.CoulombBranch.stripEntropy_phase_transition` : the first-order transition at `ℓ_c`.
+- `DBrane.CoulombBranch.stripEntropy_saturates` : the regulated entropy is `ℓ`-independent
+  for `ℓ > ℓ_c`.
+- `DBrane.CoulombBranch.stripEntropy_uv_divergence` : the leading UV divergence is an area
+  law matching the throat vacuum.
+- `DBrane.CoulombBranch.entropicCFunction_throat_running` : the running of the c-function in
+  the throat regime.
+- `DBrane.CoulombBranch.entropicCFunction_vanishes_in_bubble` : the c-function vanishes for
+  `ℓ > ℓ_c`.
+
+## iii. Table of contents
+
+- A. The area functional for strip surfaces
+- B. Candidate extremal surfaces
+- C. The entanglement phase transition
+- D. UV divergences
+- E. The entropic c-function of the shell state
+
+## iv. References
+
+- E. Jørstad, R. C. Myers and S. Pasterski, *Flat Space Entanglement: A Coulomb Branch
+  Perspective*, arXiv:2606.13889, section 3.1.
+- S. Ryu and T. Takayanagi, *Aspects of Holographic Entanglement Entropy*,
+  arXiv:hep-th/0605073.
+
+-/
+
+@[expose] public section
+
+namespace DBrane
+
+namespace CoulombBranch
+
+/-!
+
+## A. The area functional for strip surfaces
+
+-/
+
+/-- The area functional for translationally invariant surfaces in the shell geometry anchored
+on a strip `-ℓ ≤ x_1 ≤ ℓ` of the boundary, described by a profile `x_1(r)`. It is the sum of
+a throat piece, for the part of the surface at `r > R`, of the schematic form
+
+`A_throat = Ω_{8-p} V_{p-1} r_p^(7-p) ∫ dr r √(1 + (r_p/r)^(7-p) x'(r)²)`
+
+and a flat piece, for the part at `r < R`, in which the harmonic function is frozen at its
+value on the shell. Extremizing this functional over profiles with the given boundary
+conditions yields the candidate RT surfaces of the strip. See section 3.1 of
+arXiv:2606.13889 for the precise expressions. -/
+informal_definition stripAreaFunctional where
+  deps := [``shellMetric, ``Holography.StripRegion]
+  tag := "GF3OU"
+
+/-- An extremal surface of `DBrane.CoulombBranch.stripAreaFunctional` crossing the shell
+`r = R` is continuous with continuous first derivative of its profile across the shell, the
+conserved momentum conjugate to `x_1` matching between the throat and flat pieces. For the
+strip this matching relates the turning points of the two pieces by an explicit power law in
+`R`; the surface refracts across the shell like a light ray crossing an interface. See
+section 3.1 of arXiv:2606.13889. -/
+informal_lemma stripRefractionCondition where
+  deps := [``stripAreaFunctional]
+  tag := "GF3OW"
+
+/-!
+
+## B. Candidate extremal surfaces
+
+-/
+
+/-- The three classes of candidate extremal surfaces for the strip in the shell geometry,
+labeled by how the surface closes off:
+
+- *throat-confined* surfaces, which turn around at a radius `r_a ≥ R` and remain entirely in
+  the throat, as for the pure throat geometry;
+- *flat-bubble* surfaces, which cross the shell and turn around smoothly at a radius
+  `0 < r_b < R` inside the flat bubble;
+- *flat-sheeted* surfaces, two parallel planar sheets which cross the shell and drop straight
+  to the origin `r = 0`, connected there through the degenerate transverse sphere.
+
+The RT surface for a given half-width `ℓ` is the least-area member among these classes. -/
+informal_definition StripSurfaceClasses where
+  deps := [``stripAreaFunctional, ``stripRefractionCondition]
+  tag := "GF3OY"
+
+/-!
+
+## C. The entanglement phase transition
+
+-/
+
+/-- The critical half-width `ℓ_c` of the strip in the shell geometry, at which the areas of
+the dominant throat-confined surface and the flat-sheeted surface coincide. It scales with
+the shell parameters as
+
+`ℓ_c ∝ (r_p/R)^((7-p)/2) R`
+
+with an explicit `p`-dependent numerical coefficient given in section 3.1 of
+arXiv:2606.13889. Up to this coefficient, `ℓ_c` is the boundary length scale dual to the
+shell radius. -/
+informal_definition criticalStripWidth where
+  deps := [``StripSurfaceClasses]
+  tag := "GF3O2"
+
+/-- The entanglement entropy of the strip in the shell geometry undergoes a first-order
+phase transition at the critical width `DBrane.CoulombBranch.criticalStripWidth`: for
+`ℓ < ℓ_c` the RT surface is throat-confined and the entropy agrees with that of the pure
+Dp-brane throat, while for `ℓ > ℓ_c` the RT surface is the flat-sheeted one. The derivative
+`dS/dℓ` jumps discontinuously at `ℓ = ℓ_c`. The flat-bubble surfaces never dominate:
+whenever they exist they have larger area than one of the other two classes. See section 3.1
+of arXiv:2606.13889. -/
+informal_lemma stripEntropy_phase_transition where
+  deps := [``criticalStripWidth, ``Holography.stripEntanglementEntropy]
+  tag := "GF3O3"
+
+/-- For `ℓ > ℓ_c` the regulated entanglement entropy of the strip in the shell geometry is
+independent of `ℓ`: the flat-sheeted RT surface consists of two rigid sheets whose regulated
+area does not change as the strip widens, so `dS/dℓ = 0`. The entanglement of the shell
+state saturates once the strip is wide enough to probe the flat-space bubble. -/
+informal_lemma stripEntropy_saturates where
+  deps := [``stripEntropy_phase_transition, ``Holography.regulatedArea]
+  tag := "GF3O5"
+
+/-!
+
+## D. UV divergences
+
+-/
+
+/-- The leading UV divergence of the strip entanglement entropy in the shell geometry is an
+area law: expressed in terms of the gauge theory cutoff `δ` of
+`DBrane.CoulombBranch.uvCutoffOfRadialCutoff`, it takes the schematic form
+
+`S ∝ N² ĝ_eff(1/δ)^(2(p-3)/(5-p)) V_{p-1}/δ^(p-1)`
+
+proportional to the area `2 V_{p-1}` of the entangling surface. It agrees with the
+divergence in the Dp-brane throat vacuum, since the shell only modifies the geometry in the
+infrared. See section 3.1 of arXiv:2606.13889 for the precise coefficient. -/
+informal_lemma stripEntropy_uv_divergence where
+  deps := [``stripAreaFunctional, ``uvCutoffOfRadialCutoff, ``DBrane.effectiveCoupling]
+  tag := "GF3O7"
+
+/-!
+
+## E. The entropic c-function of the shell state
+
+-/
+
+/-- In the throat regime `ℓ < ℓ_c` the entropic c-function of the shell state agrees with
+that of the Dp-brane throat vacuum,
+
+`c̃_p(ℓ) = N² ĝ_eff(1/(2ℓ))^(2(p-3)/(5-p))`
+
+up to a normalization: it counts `O(N²)` degrees of freedom, weighted by the running
+effective coupling at the scale of the strip. For `p = 3` this is constant, `c̃_3 ∝ N²`,
+consistent with `Holography.entropicCFunction_constant_of_cft`; for `p ≠ 3` it runs
+monotonically with `ℓ`. See section 3.1 of arXiv:2606.13889. -/
+informal_lemma entropicCFunction_throat_running where
+  deps := [``Holography.entropicCFunction, ``stripEntropy_phase_transition,
+    ``DBrane.effectiveCoupling]
+  tag := "GF3PB"
+
+/-- For `ℓ > ℓ_c` the entropic c-function of the shell state vanishes: since the regulated
+entropy saturates, `dS/dℓ = 0` and hence `c̃_p(ℓ) = 0`. The infrared degrees of freedom of
+the Coulomb-branch state are thus depleted relative to the throat vacuum: the flat-space
+bubble carries only `O(1)` degrees of freedom in the large-`N` expansion, compared with the
+`O(N²)` counted by the c-function in the throat regime. See section 3.1 of
+arXiv:2606.13889. -/
+informal_lemma entropicCFunction_vanishes_in_bubble where
+  deps := [``entropicCFunction_throat_running, ``stripEntropy_saturates]
+  tag := "GF3PD"
+
+end CoulombBranch
+
+end DBrane
+
+end
diff --git a/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/TargetSpaceEntanglement.lean b/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/TargetSpaceEntanglement.lean
new file mode 100644
index 000000000..5b1f103c7
--- /dev/null
+++ b/PhyslibAlpha/StringTheory/DBranes/CoulombBranch/TargetSpaceEntanglement.lean
@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import PhyslibAlpha.StringTheory.DBranes.CoulombBranch.Shell
+/-!
+# Target space entanglement in shell geometries
+
+## i. Overview
+
+Entanglement in a gauge theory need not be between spatial regions. In a theory of matrices —
+such as the maximally supersymmetric Yang-Mills theories dual to Dp-branes — one can instead
+partition the *target space*: the moduli space in which the eigenvalues of the adjoint
+scalars live. The entanglement between eigenvalues lying in different regions of target space
+is called target space entanglement, and for a Coulomb-branch vacuum, whose eigenvalues are
+distributed on a sphere in moduli space, it is a natural measure of correlations among the
+constituent branes.
+
+This module is built around the definition of *internal RT surfaces* in a Coulomb-branch
+shell geometry, `DBrane.CoulombBranch.InternalRTSurface`: extremal surfaces anchored on the
+brane shell itself rather than on the asymptotic boundary, lying entirely inside the
+flat-space bubble. Their areas, in units of `4 G_N`, are proposed to compute the target space
+entanglement of regions of the shell, mirroring how ordinary RT surfaces compute spatial
+entanglement. The remaining declarations are properties of these surfaces: their areas grow
+monotonically with the depth to which they penetrate the bubble, and for `p ≠ 3` the
+adjustable shell radius controls the competition between internal surfaces and surfaces
+exiting into the throat, exhibiting in target space the same infrared entanglement depletion
+that the strip and sphere calculations exhibit in position space.
+
+## ii. Key results
+
+- `DBrane.CoulombBranch.InternalRTSurface` : extremal surfaces anchored on the shell.
+- `DBrane.CoulombBranch.targetSpaceEntanglementEntropy` : the proposed target space
+  entanglement entropy computed by internal surfaces.
+- `DBrane.CoulombBranch.internalRTSurface_area_monotone` : monotonicity of the internal
+  surface area in its turning radius.
+- `DBrane.CoulombBranch.internalRTSurface_dominance` : for `p ≠ 3` the shell radius controls
+  which internal surfaces dominate.
+
+## iii. Table of contents
+
+- A. Internal RT surfaces
+- B. Target space entanglement
+- C. Monotonicity and dominance
+
+## iv. References
+
+- E. A. Mazenc and D. Ranard, *Target Space Entanglement Entropy*, arXiv:1910.07449.
+- E. Jørstad, R. C. Myers and S. Pasterski, *Flat Space Entanglement: A Coulomb Branch
+  Perspective*, arXiv:2606.13889, section 4 and appendices C, D.
+
+-/
+
+@[expose] public section
+
+namespace DBrane
+
+namespace CoulombBranch
+
+/-!
+
+## A. Internal RT surfaces
+
+-/
+
+/-- An internal RT surface of the shell geometry: an extremal surface anchored on the shell
+`r = R` (rather than on the asymptotic boundary), lying entirely inside the flat-space
+bubble `r ≤ R`, and homologous to a region of the shell. Such a surface is characterized by
+the region of the shell on which it is anchored and by its turning radius inside the bubble.
+The asymptotic behavior of these surfaces can be understood by recasting the extremal
+surface equation as the motion of a classical particle in a potential, as in appendix D of
+arXiv:2606.13889. -/
+informal_definition InternalRTSurface where
+  deps := [``shellMetric, ``shellMetric_interior_flat]
+  tag := "GF3PS"
+
+/-!
+
+## B. Target space entanglement
+
+-/
+
+/-- The target space entanglement entropy of the Coulomb-branch state associated with a
+region of the shell: the area of the corresponding internal RT surface divided by `4 G_N`.
+This computes the entanglement between subsets of the matrix (moduli space) degrees of
+freedom of the dual gauge theory, the shell being the locus of the scalar field expectation
+values of `DBrane.CoulombBranch.CoulombBranchVacuum`. See section 4 of arXiv:2606.13889 and
+the target space entanglement proposal of arXiv:1910.07449. -/
+informal_definition targetSpaceEntanglementEntropy where
+  deps := [``InternalRTSurface, ``CoulombBranchVacuum]
+  tag := "GF3PU"
+
+/-!
+
+## C. Monotonicity and dominance
+
+-/
+
+/-- The area of an internal RT surface of the shell geometry is a monotonic function of its
+turning radius inside the flat bubble: deeper surfaces subtend larger anchoring regions on
+the shell with correspondingly larger area. This monotonicity guarantees that the map from
+anchoring regions to minimal internal surfaces is well behaved. See appendix C of
+arXiv:2606.13889 for the proof. -/
+informal_lemma internalRTSurface_area_monotone where
+  deps := [``InternalRTSurface]
+  tag := "GF3PW"
+
+/-- For `p ≠ 3` the shell radius `R` is an adjustable modulus of the shell geometry, and
+tuning it controls the competition between internal RT surfaces and surfaces exiting into
+the throat: the target space entanglement of the shell state exhibits the same qualitative
+depletion in the flat-space bubble as the spatial entanglement entropy. For `p = 3` the
+proper shell size is fixed (`DBrane.CoulombBranch.properShellRadius_p3_fixed`) and no such
+tuning is available. See section 4 of arXiv:2606.13889. -/
+informal_lemma internalRTSurface_dominance where
+  deps := [``InternalRTSurface, ``targetSpaceEntanglementEntropy, ``properShellRadius_p3_fixed]
+  tag := "GF3PY"
+
+end CoulombBranch
+
+end DBrane
+
+end
diff --git a/PhyslibAlpha/StringTheory/DBranes/DecouplingLimit.lean b/PhyslibAlpha/StringTheory/DBranes/DecouplingLimit.lean
new file mode 100644
index 000000000..0553c5bb6
--- /dev/null
+++ b/PhyslibAlpha/StringTheory/DBranes/DecouplingLimit.lean
@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import PhyslibAlpha.StringTheory.DBranes.Basic
+/-!
+# The decoupling limit of Dp-branes
+
+## i. Overview
+
+The worldvolume theory of `N` coincident Dp-branes is `(p+1)`-dimensional maximally
+supersymmetric `U(N)` Yang-Mills theory. In the decoupling limit — energies far below the
+string scale, with the Yang-Mills coupling held fixed — this gauge theory decouples from the
+bulk closed strings, and is conjectured to be dual to string theory in the *throat* region of
+the Dp-brane background: the near-horizon geometry obtained by dropping the constant term in
+the harmonic function,
+
+`H(r) = (r_p/r)^(7-p)`.
+
+For `p = 3` the throat is `AdS₅ × S⁵` and the duality is the AdS/CFT correspondence with
+`𝒩 = 4` super Yang-Mills; for `p ≠ 3` the throat is conformal to `AdS_{p+2} × S^{8-p}` with a
+running dilaton, dual to a non-conformal gauge theory.
+
+Because the Yang-Mills coupling `g²_YM` has mass dimension `3 - p`, the strength of the gauge
+dynamics at an energy scale `E` is measured by the dimensionless effective coupling
+
+`ĝ²_eff(E) = g²_YM N E^(p-3)`,
+
+which runs with the scale for `p ≠ 3`. Under the holographic dictionary `E` maps to a radial
+position in the throat, and the supergravity description is valid only in the window of radii
+where the curvature is small in string units and the local string coupling is small. The
+throat is therefore a good dual of the gauge theory in an intermediate range of scales,
+matching onto other descriptions (perturbative Yang-Mills, M-theory lifts, …) outside that
+window.
+
+## ii. Key results
+
+- `DBrane.dpBraneThroatMetric` : the near-horizon throat geometry of `N` Dp-branes.
+- `DBrane.effectiveCoupling` : the running effective coupling `ĝ²_eff(E) = g²_YM N E^(p-3)` of
+  the dual gauge theory.
+- `DBrane.SupergravityRegime` : the window of scales in which the supergravity description of
+  the throat is valid.
+
+## iii. Table of contents
+
+- A. The throat geometry
+- B. The dual gauge theory coupling
+- C. Validity of the supergravity description
+
+## iv. References
+
+- N. Itzhaki, J. M. Maldacena, J. Sonnenschein and S. Yankielowicz, *Supergravity and the
+  large N limit of theories with sixteen supercharges*, arXiv:hep-th/9802042.
+- O. Aharony, S. S. Gubser, J. M. Maldacena, H. Ooguri and Y. Oz, *Large N field theories,
+  string theory and gravity*, arXiv:hep-th/9905111.
+- E. Jørstad, R. C. Myers and S. Pasterski, *Flat Space Entanglement: A Coulomb Branch
+  Perspective*, arXiv:2606.13889, section 2.2.
+
+-/
+
+@[expose] public section
+
+namespace DBrane
+
+/-!
+
+## A. The throat geometry
+
+-/
+
+/-- The throat (near-horizon) metric of `N` coincident Dp-branes: the background
+`DBrane.dpBraneMetric` with harmonic function
+
+`H(r) = (r_p/r)^(7-p)`,
+
+obtained from the stacked-brane harmonic function by dropping the constant term, as is
+appropriate at radii `r ≪ r_p` or in the decoupling limit. For `p = 3` the throat is
+`AdS₅ × S⁵` with AdS radius `L = r_3`; for `p ≠ 3` it is conformal to `AdS_{p+2} × S^{8-p}`
+with a nontrivial dilaton profile. The throat is the region of the geometry dual to
+`(p+1)`-dimensional maximally supersymmetric `U(N)` Yang-Mills theory. -/
+informal_definition dpBraneThroatMetric where
+  deps := [``dpBraneMetric]
+  tag := "GF3N7"
+
+/-!
+
+## B. The dual gauge theory coupling
+
+-/
+
+/-- The dimensionless effective coupling of `(p+1)`-dimensional maximally supersymmetric
+`U(N)` Yang-Mills theory at energy scale `E`:
+
+`ĝ²_eff(E) = g²_YM N E^(p-3)`
+
+where `g²_YM` is the Yang-Mills coupling, of mass dimension `3 - p`. For `p < 3` the coupling
+grows toward the infrared, for `p > 3` toward the ultraviolet, and for `p = 3` it is the
+'t Hooft coupling, constant by conformal invariance. Under the holographic dictionary the
+energy scale `E` corresponds to a radial position in the throat
+`DBrane.dpBraneThroatMetric`. -/
+informal_definition effectiveCoupling where
+  deps := [``dpBraneThroatMetric]
+  tag := "GF3OB"
+
+/-!
+
+## C. Validity of the supergravity description
+
+-/
+
+/-- The regime of validity of the supergravity description of the Dp-brane throat: the window
+of energy scales in which both the string-frame curvature is small in string units, requiring
+`ĝ²_eff(E) ≫ 1`, and the local string coupling is small, requiring an upper bound on
+`ĝ²_eff(E)` growing with a positive power of `N`. For `p ≠ 3` this window covers a wide but
+bounded range of scales, so the supergravity throat describes the gauge theory only at
+intermediate energies; for `p = 3` the condition is the scale-independent `1 ≪ g²_YM N ≪ N`.
+
+See arXiv:hep-th/9802042, and section 2.2 of arXiv:2606.13889. -/
+informal_definition SupergravityRegime where
+  deps := [``effectiveCoupling, ``dpBraneThroatMetric]
+  tag := "GF3OD"
+
+end DBrane
+
+end
diff --git a/PhyslibAlpha/StringTheory/Holography/Complexity.lean b/PhyslibAlpha/StringTheory/Holography/Complexity.lean
new file mode 100644
index 000000000..7df40b46b
--- /dev/null
+++ b/PhyslibAlpha/StringTheory/Holography/Complexity.lean
@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import PhyslibAlpha.StringTheory.Holography.RyuTakayanagi
+/-!
+# Holographic complexity
+
+## i. Overview
+
+Circuit complexity measures how difficult it is to prepare a quantum state from a simple
+reference state using elementary unitary operations. Holographic complexity proposals assign
+to a state of the boundary theory a bulk geometric quantity conjectured to compute this
+complexity; unlike entanglement entropy, which is blind to the interior growth of black
+holes, complexity is conjectured to probe bulk regions that RT surfaces cannot reach.
+
+The best studied proposal is *complexity equals volume* (CV):
+
+`C_V = max_Σ Vol(Σ) / (G_N ℓ_bulk)`
+
+where the maximum is over bulk codimension-one slices `Σ` anchored on the boundary time
+slice, and `ℓ_bulk` is a bulk length scale. For a static background the maximal slice is the
+constant-time slice, and the complexity reduces to the regulated volume of the bulk time
+slice — a quantity sensitive to the entire infrared geometry, complementary to the
+entanglement entropy computed by minimal surfaces.
+
+The definition in this module is background-independent, in the same spirit as
+`Holography.StaticHolographicBackground`.
+
+## ii. Key results
+
+- `Holography.complexityVolume` : the complexity-equals-volume proposal.
+
+## iii. Table of contents
+
+- A. The complexity-equals-volume proposal
+
+## iv. References
+
+- D. Stanford and L. Susskind, *Complexity and Shock Wave Geometries*, arXiv:1406.2678.
+- S. Chapman and G. Policastro, *Quantum Computational Complexity — From Quantum Information
+  to Black Holes and Back*, arXiv:2110.14672.
+
+-/
+
+@[expose] public section
+
+namespace Holography
+
+/-!
+
+## A. The complexity-equals-volume proposal
+
+-/
+
+/-- The complexity-equals-volume (CV) proposal: the holographic complexity of the boundary
+state on a time slice is
+
+`C_V = max_Σ Vol(Σ) / (G_N ℓ_bulk)`
+
+where the maximum is over bulk codimension-one slices `Σ` anchored on the boundary time
+slice, the volume is computed with the Einstein-frame metric, and `ℓ_bulk` is a bulk length
+scale (for AdS, the AdS radius). For a static background the maximal slice is the
+constant-time slice. Like the entanglement entropy, the complexity is UV divergent and is
+regulated by evaluating the volume inside the cutoff surface `r = r_uv`. -/
+informal_definition complexityVolume where
+  deps := [``StaticHolographicBackground]
+  tag := "GF3P2"
+
+end Holography
+
+end
diff --git a/PhyslibAlpha/StringTheory/Holography/EntropicCFunction.lean b/PhyslibAlpha/StringTheory/Holography/EntropicCFunction.lean
new file mode 100644
index 000000000..3ced08d68
--- /dev/null
+++ b/PhyslibAlpha/StringTheory/Holography/EntropicCFunction.lean
@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import PhyslibAlpha.StringTheory.Holography.RyuTakayanagi
+/-!
+# Entropic c-functions
+
+## i. Overview
+
+The entanglement entropy of a strip-shaped region probes a quantum field theory at a single
+length scale: the width of the strip. Its UV divergences are independent of the width, so the
+derivative of the entropy with respect to the width is cutoff-independent, and suitably
+normalized it defines an *entropic c-function*
+
+`c̃_p(ℓ) = β_p (ℓ^p / V_{p-1}) dS(ℓ)/dℓ`
+
+for a `(p+1)`-dimensional theory, with `ℓ` the half-width of the strip and `V_{p-1}` the
+regulated volume of its cross-section. The c-function measures the number of effective
+degrees of freedom at the scale `ℓ`: for a conformal theory it is constant and proportional
+to the central charge, while along a renormalization group flow it interpolates between the
+ultraviolet and infrared degrees of freedom. In `d = 2` the Casini-Huerta entropic c-theorem
+shows the interpolation is monotonic, giving an entanglement proof of Zamolodchikov's
+c-theorem.
+
+In a holographic theory the strip entropy `S(ℓ)` is computed by the RT prescription, and the
+c-function becomes a diagnostic of the dual geometry: it is sensitive to the bulk region
+reached by the RT surface of a strip of width `2ℓ`, so its running with `ℓ` traces how the
+number of degrees of freedom changes with depth in the bulk. A c-function which vanishes
+beyond some width signals an infrared region of the geometry carrying parametrically fewer
+degrees of freedom than the ultraviolet.
+
+## ii. Key results
+
+- `Holography.StripRegion` : the strip-shaped boundary region of half-width `ℓ`.
+- `Holography.stripEntanglementEntropy` : the entanglement entropy of the strip as a function
+  of `ℓ`.
+- `Holography.entropicCFunction` : the entropic c-function built from the strip entanglement
+  entropy.
+- `Holography.entropicCFunction_constant_of_cft` : for a conformal boundary theory the
+  entropic c-function is constant, proportional to the central charge.
+
+## iii. Table of contents
+
+- A. Strip regions and their entanglement entropy
+- B. The entropic c-function
+
+## iv. References
+
+- H. Casini and M. Huerta, *A c-theorem for the entanglement entropy*,
+  arXiv:cond-mat/0610375.
+- S. Ryu and T. Takayanagi, *Aspects of Holographic Entanglement Entropy*,
+  arXiv:hep-th/0605073.
+- E. Jørstad, R. C. Myers and S. Pasterski, *Flat Space Entanglement: A Coulomb Branch
+  Perspective*, arXiv:2606.13889, section 3.1.
+
+-/
+
+@[expose] public section
+
+namespace Holography
+
+/-!
+
+## A. Strip regions and their entanglement entropy
+
+-/
+
+/-- The strip region of half-width `ℓ` on a `d`-dimensional boundary theory: on a fixed time
+slice with spatial coordinates `(x_1, …, x_{d-1})`, the region
+
+`A = {-ℓ ≤ x_1 ≤ ℓ}`
+
+with the remaining coordinates unrestricted (or regulated to have finite volume `V_{d-2}`).
+The entangling surface consists of the two parallel planes `x_1 = ±ℓ`, so the strip probes
+the theory at the single length scale `2ℓ`. -/
+informal_definition StripRegion where
+  deps := [``BoundaryRegion]
+  tag := "GF3NK"
+
+/-- The entanglement entropy `S(ℓ)` of the strip region of half-width `ℓ`, obtained from the
+RT prescription applied to `Holography.StripRegion`, as a function of `ℓ`. Because the strip
+is translationally invariant along the entangling surface, the RT surface is determined by a
+single profile function `x_1(r)` of the bulk radial coordinate, and `S(ℓ)` reduces to a
+one-dimensional variational problem with a conserved momentum, integrable by quadrature. -/
+informal_definition stripEntanglementEntropy where
+  deps := [``StripRegion, ``holographicEntanglementEntropy]
+  tag := "GF3NM"
+
+/-!
+
+## B. The entropic c-function
+
+-/
+
+/-- The entropic c-function of a `(p+1)`-dimensional boundary theory: for a strip of
+half-width `ℓ` and regulated transverse volume `V_{p-1}`,
+
+`c̃_p(ℓ) = β_p (ℓ^p / V_{p-1}) dS(ℓ)/dℓ`
+
+where `β_p` is a `p`-dependent normalization constant. The UV divergences of `S(ℓ)` are
+`ℓ`-independent, so `c̃_p` is cutoff-independent; it measures the number of effective degrees
+of freedom of the boundary theory at the length scale `ℓ`. -/
+informal_definition entropicCFunction where
+  deps := [``stripEntanglementEntropy]
+  tag := "GF3NO"
+
+/-- For a conformal boundary theory the entropic c-function is independent of the strip width
+`ℓ`, and with a suitable choice of the normalization `β_p` it equals a multiple of the
+central charge `C_T` of the conformal field theory. For example, for `p = 3`
+(four-dimensional `𝒩 = 4` super Yang-Mills) one finds `c̃_3 = 4 C_T ∝ N²`. -/
+informal_lemma entropicCFunction_constant_of_cft where
+  deps := [``entropicCFunction]
+  tag := "GF3NQ"
+
+end Holography
+
+end
diff --git a/PhyslibAlpha/StringTheory/Holography/FlatSpaceRT.lean b/PhyslibAlpha/StringTheory/Holography/FlatSpaceRT.lean
new file mode 100644
index 000000000..438fd093f
--- /dev/null
+++ b/PhyslibAlpha/StringTheory/Holography/FlatSpaceRT.lean
@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import PhyslibAlpha.StringTheory.Holography.RyuTakayanagi
+/-!
+# Ryu-Takayanagi surfaces in flat space
+
+## i. Overview
+
+Minkowski space can be treated as a static holographic background by placing boundary regions
+on a large sphere of radius `r_uv` and applying the Ryu-Takayanagi prescription. The outcome
+differs sharply from the asymptotically anti-de Sitter case, for a simple geometric reason: a
+constant-time slice of Minkowski space is flat Euclidean space, so there is no gravitational
+potential to bend minimal surfaces, and the minimal surface anchored on the boundary of a
+region of the cutoff sphere is a flat hyperplane.
+
+Two consequences follow. First, the entanglement entropy of a spherical cap scales with the
+*volume* of the cap on the cutoff sphere,
+
+`S(A) ∝ r_uv^(d-1) Ω_A / G_N`,
+
+a volume law, in contrast with the area law `S(A) ∝ Area(∂A)` of asymptotically AdS
+backgrounds. Second, the flat hyperplane surfaces hug the cutoff sphere and never descend far
+into the interior, so holographic entanglement entropy in flat space is a poor probe of deep
+infrared bulk physics. Both features are recurring puzzles for any attempt at flat-space
+holography, and both are made quantitative by the definitions in this module. A controlled
+setting in which a flat region arises as the infrared of a standard holographic background is
+provided by the Coulomb-branch shell geometries of
+`PhyslibAlpha.StringTheory.DBranes.CoulombBranch.Shell`.
+
+## ii. Key results
+
+- `Holography.MinkowskiBackground` : Minkowski space as a static holographic background.
+- `Holography.rtSurface_flat_hyperplane` : minimal surfaces in a flat time slice are flat
+  hyperplanes.
+- `Holography.flat_cap_entropy_volume_law` : the RT entropy of a spherical cap in flat space
+  obeys a volume law in the cutoff radius.
+
+## iii. Table of contents
+
+- A. Minkowski space as a holographic background
+- B. Minimal surfaces in flat space
+- C. The volume law
+
+## iv. References
+
+- W. Li and T. Takayanagi, *Holography and Entanglement in Flat Spacetime*,
+  arXiv:1010.3700.
+- E. Jørstad, R. C. Myers and S. Pasterski, *Flat Space Entanglement: A Coulomb Branch
+  Perspective*, arXiv:2606.13889, section 2.1.
+
+-/
+
+@[expose] public section
+
+namespace Holography
+
+/-!
+
+## A. Minkowski space as a holographic background
+
+-/
+
+/-- `(d+1)`-dimensional Minkowski space regarded as a static holographic background: the
+constant-time slice is flat Euclidean space, with metric in polar coordinates
+
+`ds² = dr² + r² (dθ² + cos²θ dΩ²_{d-2})`,
+
+the cutoff surface is the sphere `r = r_uv`, and boundary regions are regions of this sphere.
+This is the setting in which the Ryu-Takayanagi prescription is applied directly to flat
+space. -/
+informal_definition MinkowskiBackground where
+  deps := [``StaticHolographicBackground]
+  tag := "GF3QB"
+
+/-!
+
+## B. Minimal surfaces in flat space
+
+-/
+
+/-- In the flat background `Holography.MinkowskiBackground`, a minimal surface anchored on
+the boundary of a spherical cap of the cutoff sphere `r = r_uv` is a flat hyperplane: with no
+gravitational potential to bend the surface, the variational problem for the RT surface is
+solved by totally geodesic hyperplanes. In particular the surface remains at distances of
+order `r_uv` from the origin and does not probe the deep interior of the bulk. -/
+informal_lemma rtSurface_flat_hyperplane where
+  deps := [``MinkowskiBackground, ``RTSurface]
+  tag := "GF3NS"
+
+/-!
+
+## C. The volume law
+
+-/
+
+/-- For a spherical cap `A` of opening angle `θ_0` on the cutoff sphere `r = r_uv` of the
+flat background `Holography.MinkowskiBackground`, the RT entropy scales as
+
+`S(A) ∝ r_uv^(d-1) Ω_A / G_N`
+
+where `Ω_A` is the solid angle subtended by `A`. This is a *volume law* in the boundary
+region `A`, in contrast with the area law of asymptotically AdS backgrounds: the leading
+divergence is proportional to the volume of `A` rather than the area of the entangling
+surface `∂A`. See section 2.1 of arXiv:2606.13889. -/
+informal_lemma flat_cap_entropy_volume_law where
+  deps := [``MinkowskiBackground, ``rtSurface_flat_hyperplane, ``holographicEntanglementEntropy]
+  tag := "GF3NU"
+
+end Holography
+
+end
diff --git a/PhyslibAlpha/StringTheory/Holography/RyuTakayanagi.lean b/PhyslibAlpha/StringTheory/Holography/RyuTakayanagi.lean
new file mode 100644
index 000000000..0fce9caa2
--- /dev/null
+++ b/PhyslibAlpha/StringTheory/Holography/RyuTakayanagi.lean
@@ -0,0 +1,158 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import Physlib.Meta.Informal.Basic
+/-!
+# The Ryu-Takayanagi prescription
+
+## i. Overview
+
+In a holographic duality, the entanglement entropy of a spatial region `A` of the boundary
+theory is computed by a purely geometric quantity in the bulk. The Ryu-Takayanagi (RT)
+prescription states that
+
+`S(A) = min_{γ ∼ A} Area(γ) / (4 G_N)`
+
+where the minimum is over bulk codimension-two surfaces `γ` anchored on the entangling surface
+`∂A` and homologous to `A`, and `G_N` is the bulk Newton constant. The formula generalizes the
+Bekenstein-Hawking entropy of horizons to arbitrary boundary regions, and reduces questions
+about the entanglement structure of strongly coupled states to variational problems for
+minimal surfaces in the dual geometry.
+
+Several structural features follow directly from the prescription. The entropy is UV
+divergent, the divergence governed by the geometry near the cutoff surface on which `A` is
+specified. Several extremal surfaces may satisfy the anchoring and homology conditions, and
+exchanges of dominance between them as `A` is varied produce entanglement analogues of phase
+transitions. Both features carry physical information: the divergence structure encodes the
+local degrees of freedom of the boundary theory, and dominance exchanges diagnose scales at
+which its infrared structure changes.
+
+The definitions in this module are deliberately independent of any particular bulk solution
+and of the shape of the boundary region, so that they can be instantiated for anti-de Sitter
+space, Dp-brane throats, Coulomb-branch shell geometries, or any other static holographic
+background.
+
+## ii. Key results
+
+- `Holography.StaticHolographicBackground` : the bulk data on which the RT prescription is
+  evaluated.
+- `Holography.BoundaryRegion` : a region of a fixed time slice of the boundary theory.
+- `Holography.RTSurface` : the minimal-area bulk surface anchored on, and homologous to, a
+  boundary region.
+- `Holography.holographicEntanglementEntropy` : the entanglement entropy assigned to a
+  boundary region by the RT prescription.
+- `Holography.regulatedArea` : the area of an RT surface with its UV-divergent part
+  subtracted.
+
+## iii. Table of contents
+
+- A. The holographic background
+- B. Boundary regions
+- C. Ryu-Takayanagi surfaces
+- D. Holographic entanglement entropy
+
+## iv. References
+
+- S. Ryu and T. Takayanagi, *Holographic derivation of entanglement entropy from AdS/CFT*,
+  arXiv:hep-th/0603001.
+- T. Nishioka, S. Ryu and T. Takayanagi, *Holographic Entanglement Entropy: An Overview*,
+  arXiv:0905.0932.
+- M. Rangamani and T. Takayanagi, *Holographic Entanglement Entropy*, arXiv:1609.01287.
+
+-/
+
+@[expose] public section
+
+namespace Holography
+
+/-!
+
+## A. The holographic background
+
+-/
+
+/-- The data of a static holographic background on which the Ryu-Takayanagi prescription is
+evaluated. This consists of:
+
+- a Riemannian manifold `M`, the constant-time slice of a static bulk spacetime (possibly
+  including compact internal directions, as for ten-dimensional brane geometries);
+- a bulk Newton constant `G_N`;
+- a distinguished radial coordinate `r` together with a cutoff surface `r = r_uv` near the
+  asymptotic region, on which boundary regions are specified.
+
+Staticity ensures that the covariant (HRT) prescription reduces to a minimal-surface problem
+on the time slice. The asymptotic region may be anti-de Sitter, a Dp-brane throat, or flat
+space; the cutoff surface regulates the infinite volume near it in all three cases. -/
+informal_definition StaticHolographicBackground where
+  deps := []
+  tag := "GF3M5"
+
+/-!
+
+## B. Boundary regions
+
+-/
+
+/-- A region `A` of the cutoff surface of a static holographic background, specified on a
+fixed time slice. The boundary `∂A` of the region within the cutoff surface is called the
+*entangling surface*. Typical examples are the strip, bounded by two parallel planes, and the
+ball, bounded by a sphere; the shape of `A` determines the symmetry of the associated minimal
+surface problem. -/
+informal_definition BoundaryRegion where
+  deps := [``StaticHolographicBackground]
+  tag := "GF3NC"
+
+/-!
+
+## C. Ryu-Takayanagi surfaces
+
+-/
+
+/-- The Ryu-Takayanagi surface of a boundary region `A` in a static holographic background:
+the codimension-two bulk surface `γ` (codimension one in the constant-time slice) of minimal
+area among surfaces which
+
+- are anchored on the entangling surface, `∂γ = ∂A`, and
+- are homologous to `A`, i.e. there is a bulk region whose boundary is `γ ∪ A`.
+
+The area is computed with the Einstein-frame bulk metric restricted to the time slice. In
+general several extremal surfaces satisfy these conditions, and the RT surface is the one of
+least area; as `A` is varied, exchanges of dominance between competing extremal surfaces
+produce non-analytic behavior of the entanglement entropy. -/
+informal_definition RTSurface where
+  deps := [``StaticHolographicBackground, ``BoundaryRegion]
+  tag := "GF3NE"
+
+/-!
+
+## D. Holographic entanglement entropy
+
+-/
+
+/-- The holographic entanglement entropy of a boundary region `A`:
+
+`S(A) = Area(γ_A) / (4 G_N)`
+
+where `γ_A` is the RT surface of `A`. Via the Ryu-Takayanagi conjecture this equals the von
+Neumann entropy of the reduced state of the boundary theory on `A`. -/
+informal_definition holographicEntanglementEntropy where
+  deps := [``RTSurface]
+  tag := "GF3NG"
+
+/-- The regulated area of an RT surface: the area evaluated with the anchoring moved to the
+cutoff surface `r = r_uv`, with the divergent terms as `r_uv → ∞` subtracted. For
+asymptotically AdS backgrounds the leading divergence is an area law in the entangling
+surface; for asymptotically flat regions it is instead a volume law in the boundary region
+(see `Holography.flat_cap_entropy_volume_law`). The regulated area isolates the
+cutoff-independent information in the entanglement entropy. -/
+informal_definition regulatedArea where
+  deps := [``RTSurface, ``holographicEntanglementEntropy]
+  tag := "GF3NI"
+
+end Holography
+
+end