Conformal invariance of the two-surface extrinsic density

Proved

QAlgorithms.Papers.Independent.Intakethird100.P26.extrinsic_conformal_density_invariant

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

prove2quantum

For a two-dimensional surface in a four-dimensional Riemannian manifold, let $\sigma$ be its positive definite induced metric matrix in tangent coordinates and let $k_i$ ( $i=1,2$ ) be the two symmetric covariant second fundamental forms for orthonormal normals. Define

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

For a Weyl factor $\omega$ and normal derivatives $v_i=n_i(\omega)$ , use the source convention $\sigma^\prime=e^{-2\omega}\sigma$ and $k_i^\prime=e^{-\omega}(k_i+v_i\sigma)$ . Then

\sqrt{\det\sigma^\prime}\,Q(\sigma^\prime,k^\prime)=\sqrt{\det\sigma}\,Q(\sigma,k).

This local density identity gives the conformal invariance of its integral over a smooth closed surface. It leaves the physical anomaly coefficient undetermined.

Formalization Note The assertion is the coordinate tensor identity at each point, valid for every positive definite metric and pair of symmetric covariant forms. It therefore needs no global tangent chart or normal frame. The bare scalar has weight +2; the plan’s density interpretation is used.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P26

Formal statement

noncomputable section

open Set

namespace QAlgorithms.Papers.Independent.Intakethird100.P26

/-- PDF p.13, after (4.5), with the second fundamental form convention
printed above (4.5). The invariant is the area-weighted density: the bare
scalar has conformal weight +2. This is a fibrewise tensor identity in local
coordinates, so it applies to every smooth closed embedded two-surface of
the source without a choice of a global coordinate chart or normal frame.
Its pointwise equality gives invariance of the integrated density.
Printed: the combination `(k^i)^2 - 2Tr(k^i k^i)` is conformally invariant.
Changed: assert invariance of its induced area-weighted density.
Why: the printed transformation gives the scalar weight +2, canceled exactly
by the two-dimensional area weight -2, as required by the integrated anomaly
argument. No change to (4.4) or determination of lambda is asserted. -/
theorem extrinsic_conformal_density_invariant
    (sigma : Matrix (Fin 2) (Fin 2) ℝ) (hsigma : sigma.PosDef)
    (k : Fin 2 → Matrix (Fin 2) (Fin 2) ℝ)
    (hk : ∀ i, (k i).IsSymm) (omega : ℝ) (v : Fin 2 → ℝ) :
    extrinsicDensity (weylSurfaceMetric omega sigma)
      (weylSecondForms omega v sigma k) = extrinsicDensity sigma k := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P26

end

Source

Proof of the Holographic Formula for Entanglement Entropy, arXiv:hep-th/0606184v2, PDF p. 13, Section 4, after (4.5)

Read-back

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

For every real symmetric positive definite $2\times2$ matrix $\sigma$ , meaning $z^{\mathsf T}\sigma z>0$ for every nonzero $z\in\mathbb R^2$ , every pair of real symmetric $2\times2$ matrices $k_0,k_1$ , every real number $\omega$ , and every vector $v=(v_0,v_1)\in\mathbb R^2$ , set $\widetilde{\sigma}=e^{-2\omega}\sigma$ and $\widetilde{k}_i=e^{-\omega}(k_i+v_i\sigma)$ for $i=0,1$ . Then

\sqrt{\det\widetilde{\sigma}}\, \sum_{i=0}^{1} \left( \bigl(\operatorname{tr}(\widetilde{\sigma}^{-1}\widetilde{k}_i)\bigr)^2 - 2\operatorname{tr}\bigl( (\widetilde{\sigma}^{-1}\widetilde{k}_i) (\widetilde{\sigma}^{-1}\widetilde{k}_i) \bigr) \right) = \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 further restrictions on $\omega$ , $v$ , or the symmetric matrices $k_i$ .

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