Prove2Me

Identity (82)–(83) — divergence form of (Δf)2−∥fij∥2−2Λ(\Delta f)^2-\|f_{ij}\|^2-2\Lambda

Proved
FlatlyFoliated.identity_82_83

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

elliptic-pdegeneral-relativitymathematical-physics

For every smooth f:R3→Rf:\mathbb R^3\to\mathbb R and every Λ∈R\Lambda\in\mathbb R,

∇⋅(Δf ∇f−Hess⁡f(∇f,⋅)−Λ3⋅2r∂r)=(Δf)2−∥fij∥2−2Λ,\nabla\cdot\Big(\Delta f\,\nabla f-\operatorname{Hess}f(\nabla f,\cdot)-\tfrac{\Lambda}{3}\cdot2r\partial_r\Big)=(\Delta f)^2-\|f_{ij}\|^2-2\Lambda,

where r∂rr\partial_r is the position vector field xx. In coordinates the vector field has components Δf fj−∑ifijfi−2Λ3xj\Delta f\,f_j-\sum_i f_{ij}f_i-\tfrac{2\Lambda}{3}x_j.

This identity drives the divergence-theorem argument in the proof of Theorem 5.

Preamble
import Mathlib
import Definitions.Def_FlatlyFoliatedRelativity_basic

open scoped ContDiff
Formal statement
namespace FlatlyFoliated

/-- Identity (82)–(83):
`∇·(Δf ∇f − Hess f(∇f,·) − (Λ/3)·2r∂ᵣ) = (Δf)² − ‖fᵢⱼ‖² − 2Λ`. -/
theorem identity_82_83 (Λ : ℝ) (f : R3 → ℝ) (hf : ContDiff ℝ ∞ f) (x : R3) :
    ∑ j, pd j (fun y => lap f y * pd j f y - ∑ i, pd j (pd i f) y * pd i f y
        - (2 * Λ / 3) * y j) x =
      lap f x ^ 2 - hessNormSq f x - 2 * Λ := by sorry

end FlatlyFoliated
Source
Bray, Hamm, Hirsch, Wheeler, Zhang, Flatly Foliated Relativity, arXiv:1911.00967v2, https://arxiv.org/abs/1911.00967, p. 17, equations (82)–(83)
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph