Definitions for Proof of the Holographic Formula for Entanglement Entropy

Definition

QAlgorithms_Papers_Independent_Intakethird100_P26

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

The objects the formalized statements of Proof of the Holographic Formula for Entanglement Entropy (arXiv:hep-th/0606184) are stated in. Each was checked against the paper by a blind read-back and a moderator.

btzSliceEnergy: PDF pp.8–9, (2.13): kinetic energy of the actual constant-tau BTZ slice, in lifted coordinates q=(rho,phi). The metric is d rho^2 + rplus^2 * cosh(rho/l)^2 * d phi^2. The angular coordinate is projected modulo 2*pi at the endpoints.
IsBTZSliceGeodesic: PDF pp.8–9, (2.13): affine geodesics of the BTZ slice, defined by the Euler–Lagrange equation of its kinetic energy, rather than by an assumed turning property. Only interior derivatives are used; the curve is C^2 up to the endpoints.
extrinsicQuadratic: PDF p.13, the combination following (4.5): sum over both orthonormal normal directions of squared mean curvature minus twice squared second fundamental form. sigma and k i are the covariant 2-by-2 component matrices in any tangent coordinate basis; sigma is required positive definite by the theorem. Matrix inverse raises one tangent index.
extrinsicDensity: PDF pp.12–13: the coordinate area density multiplying the conformal extrinsic invariant. The square root is of the determinant of the induced positive definite metric, not of an arbitrary signed tensor.
weylSurfaceMetric: PDF p.12: the induced metric under h -> exp(-2*omega) h.
weylSecondForms: PDF p.13, displayed second fundamental form transformation: v i is the old unit-normal derivative n_i(omega). Both normal covariant forms transform, with the source's plus sign.

Definition code

import Mathlib

/-!
Fursaev, arXiv:hep-th/0606184v2. This module states the BTZ turning result
and the algebraic conformal density identity. Physical entropy identifications
and the unconstructed global geometric interfaces are deferred in the unit.
Complementary pure-state entropy equality is reused through metadata only.
-/

noncomputable section

open Set

namespace QAlgorithms.Papers.Independent.Intakethird100.P26

/-- PDF pp.8–9, (2.13): kinetic energy of the actual constant-tau BTZ slice,
in lifted coordinates q=(rho,phi). The metric is
`d rho^2 + rplus^2 * cosh(rho/l)^2 * d phi^2`.
The angular coordinate is projected modulo `2*pi` at the endpoints. -/
def btzSliceEnergy (l rplus : ℝ) (q v : Fin 2 → ℝ) : ℝ :=
  (v 0 ^ 2 + rplus ^ 2 * Real.cosh (q 0 / l) ^ 2 * v 1 ^ 2) / 2

/-- PDF pp.8–9, (2.13): affine geodesics of the BTZ slice, defined by the
Euler–Lagrange equation of its kinetic energy, rather than by an assumed
turning property. Only interior derivatives are used; the curve is C^2 up
to the endpoints. -/
def IsBTZSliceGeodesic (l rplus a b : ℝ) (x : ℝ → (Fin 2 → ℝ)) : Prop :=
  ContDiffOn ℝ 2 x (Icc a b) ∧
    ∀ t ∈ Ioo a b, ∀ j : Fin 2,
      deriv (fun s =>
        (fderiv ℝ (fun v => btzSliceEnergy l rplus (x s) v) (deriv x s))
          (Pi.single j 1)) t =
      (fderiv ℝ (fun q => btzSliceEnergy l rplus q (deriv x t)) (x t))
        (Pi.single j 1)

example (l rplus : ℝ) (q : Fin 2 → ℝ) :
    btzSliceEnergy l rplus q 0 = 0 := by
  simp [btzSliceEnergy]

example (l rplus : ℝ) (v : Fin 2 → ℝ) :
    btzSliceEnergy l rplus 0 v = (v 0 ^ 2 + rplus ^ 2 * v 1 ^ 2) / 2 := by
  simp [btzSliceEnergy]

/-- PDF p.13, the combination following (4.5): sum over both orthonormal
normal directions of squared mean curvature minus twice squared second
fundamental form. `sigma` and `k i` are the covariant 2-by-2 component
matrices in any tangent coordinate basis; `sigma` is required positive
definite by the theorem. Matrix inverse raises one tangent index. -/
def extrinsicQuadratic (sigma : Matrix (Fin 2) (Fin 2) ℝ)
    (k : Fin 2 → Matrix (Fin 2) (Fin 2) ℝ) : ℝ :=
  ∑ i : Fin 2,
    ((Matrix.trace (sigma⁻¹ * k i)) ^ 2 -
      2 * Matrix.trace ((sigma⁻¹ * k i) * (sigma⁻¹ * k i)))

/-- PDF pp.12–13: the coordinate area density multiplying the conformal
extrinsic invariant. The square root is of the determinant of the induced
positive definite metric, not of an arbitrary signed tensor. -/
def extrinsicDensity (sigma : Matrix (Fin 2) (Fin 2) ℝ)
    (k : Fin 2 → Matrix (Fin 2) (Fin 2) ℝ) : ℝ :=
  Real.sqrt sigma.det * extrinsicQuadratic sigma k

/-- PDF p.12: the induced metric under `h -> exp(-2*omega) h`. -/
def weylSurfaceMetric (omega : ℝ)
    (sigma : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=
  Real.exp (-2 * omega) • sigma

/-- PDF p.13, displayed second fundamental form transformation:
`v i` is the old unit-normal derivative `n_i(omega)`. Both normal
covariant forms transform, with the source's plus sign. -/
def weylSecondForms (omega : ℝ) (v : Fin 2 → ℝ)
    (sigma : Matrix (Fin 2) (Fin 2) ℝ)
    (k : Fin 2 → Matrix (Fin 2) (Fin 2) ℝ) :
    Fin 2 → Matrix (Fin 2) (Fin 2) ℝ :=
  fun i => Real.exp (-omega) • (k i + v i • sigma)

example (sigma : Matrix (Fin 2) (Fin 2) ℝ) :
    extrinsicDensity sigma (fun _ => 0) = 0 := by
  simp [extrinsicDensity, extrinsicQuadratic]

example (v : Fin 2 → ℝ) (sigma : Matrix (Fin 2) (Fin 2) ℝ)
    (k : Fin 2 → Matrix (Fin 2) (Fin 2) ℝ) :
    weylSecondForms 0 v sigma k = fun i => k i + v i • sigma := by
  funext i
  change Real.exp (-(0 : ℝ)) • (k i + v i • sigma) = k i + v i • sigma
  rw [neg_zero, Real.exp_zero, one_smul]

end QAlgorithms.Papers.Independent.Intakethird100.P26

Source

Proof of the Holographic Formula for Entanglement Entropy, arXiv:hep-th/0606184v2, https://arxiv.org/abs/hep-th/0606184v2

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

`QAlgorithms.Papers.Independent.Intakethird100.P26.IsBTZSliceGeodesic`

For arbitrary real numbers $l,r_+,a,b$ and a function $x:\mathbb R\to\mathbb R^2$ , this defines a property requiring that $x$ be twice continuously differentiable within the closed interval $[a,b]$ , and that, for every $t\in(a,b)$ and each $j\in\{0,1\}$ ,

\left.\frac{d}{ds}\left(D_vE_{l,r_+}(x(s),x'(s))[e_j]\right)\right|_{s=t} = D_qE_{l,r_+}(x(t),x'(t))[e_j], \qquad E_{l,r_+}(q,v)=\frac{v_0^2+r_+^2\cosh^2(q_0/l)\,v_1^2}{2}.

Here $e_j$ is the vector with coordinate $1$ at $j$ and $0$ at the other coordinate, and $D_v,D_q$ denote the Fréchet derivatives in the indicated vector argument, with the other argument held fixed. Derivatives are total operations, assigned zero when the required derivative does not exist. No ordering of $a,b$ or positivity of $l,r_+$ is assumed; division by zero is assigned zero. If $a\ge b$ , the differential-equation requirement is vacuous, and if $a>b$ , the closed interval is also empty, so the entire property holds for every $x$ .

`QAlgorithms.Papers.Independent.Intakethird100.P26.btzSliceEnergy`

For arbitrary real numbers $l,r_+$ and vectors $q=(q_0,q_1),v=(v_0,v_1)\in\mathbb R^2$ , this defines the real number

E_{l,r_+}(q,v)=\frac{v_0^2+r_+^2\cosh^2(q_0/l)\,v_1^2}{2}.

There are no positivity or nonzero assumptions on $l$ or $r_+$ , and the expression does not depend on $q_1$ . Division uses the total real-number convention, so when $l=0$ , $q_0/l=0$ and the value is $(v_0^2+r_+^2v_1^2)/2$ .

`QAlgorithms.Papers.Independent.Intakethird100.P26.extrinsicDensity`

For an arbitrary real $2\times2$ matrix $\sigma$ and a pair $k_0,k_1$ of real $2\times2$ matrices, this defines

\sqrt{\det\sigma}\, \sum_{i=0}^{1} \left( \bigl(\operatorname{tr}(\sigma^{-1}k_i)\bigr)^2 - 2\operatorname{tr}\bigl((\sigma^{-1}k_i)(\sigma^{-1}k_i)\bigr) \right).

There are no symmetry, positivity, or invertibility assumptions. The real square root is assigned zero for negative inputs, and the total matrix inverse is zero for singular matrices; in particular, this density is zero whenever $\det\sigma\le0$ .

`QAlgorithms.Papers.Independent.Intakethird100.P26.extrinsicQuadratic`

For an arbitrary real $2\times2$ matrix $\sigma$ and a pair $k_0,k_1$ of real $2\times2$ matrices, this defines

Q(\sigma,k)= \sum_{i=0}^{1} \left( \bigl(\operatorname{tr}(\sigma^{-1}k_i)\bigr)^2 - 2\operatorname{tr}\bigl((\sigma^{-1}k_i)(\sigma^{-1}k_i)\bigr) \right).

All products inside the traces are matrix products. There are no symmetry, positivity, or invertibility assumptions. The matrix inverse is total: when $\sigma$ is singular its inverse is the zero matrix, so this expression is zero.

`QAlgorithms.Papers.Independent.Intakethird100.P26.weylSecondForms`

For every real number $\omega$ , every vector $v=(v_0,v_1)\in\mathbb R^2$ , every real $2\times2$ matrix $\sigma$ , and every pair $k_0,k_1$ of real $2\times2$ matrices, this defines a pair of matrices by

\widetilde{k}_i=e^{-\omega}(k_i+v_i\sigma) \qquad(i\in\{0,1\}).

The real factors act by entrywise scalar multiplication. No symmetry, positivity, or invertibility conditions are imposed on these inputs.

`QAlgorithms.Papers.Independent.Intakethird100.P26.weylSurfaceMetric`

For every real number $\omega$ and every real $2\times2$ matrix $\sigma$ , this defines the real $2\times2$ matrix

\widetilde{\sigma}=e^{-2\omega}\sigma,

where scalar multiplication multiplies every entry of $\sigma$ by $e^{-2\omega}$ . No symmetry, positivity, or invertibility condition on $\sigma$ is imposed.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph