Spatial Poincaré lemma: integrate a spatially closed Hessian on $\mathbb{R}^4$

import Definitions.Def_NewtonCartan_defs

open scoped ContDiff

namespace NewtonCartan

/-- If $F^a{}_d$ is smooth, vanishes on temporal indices, is symmetric, and is closed as a Hessian in
spatial indices, then there is smooth $\varphi$ with $\partial_j\partial_i\varphi = F^i{}_j$ for spatial $i,j$
(equivalently $\partial_j(\nabla^i\varphi)=F^i{}_j$). -/
theorem exists_potential_of_spatial_F (F : E → Fin 4 → Fin 4 → ℝ)
    (hF : ContDiff ℝ ∞ F)
    (hrow : ∀ x d, F x 0 d = 0) (hcol : ∀ x a, F x a 0 = 0)
    (hsym : ∀ x i j, F x i j = F x j i)
    (hclosed : ∀ x i j k, i ≠ 0 → j ≠ 0 → k ≠ 0 →
      pd (fun y => F y i j) k x = pd (fun y => F y i k) j x) :
    ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧
      ∀ x i j, i ≠ 0 → j ≠ 0 →
        pd (fun y => gradUp φ y i) j x = F x i j := by sorry

end NewtonCartan