Cancellation of the directed screened face terms

Pairing the two cell orientations cancels the common potential trace and leaves the normal derivative jump, with coefficient exactly minus 4 pi times the landed face density.

theorem LiebThirring.bisectorNormal_reverse {M : ℕ} (R : Fin M → Position) (k l : Fin M) : bisectorNormal R l k = -bisectorNormal R k l

theorem LiebThirring.screenedCellBoundaryTerm_pair {M : ℕ} (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (f : Position → ℝ) {x : Position} (hx : x ∈ voronoiFace R k l) : screenedCellBoundaryTerm Z R k l f x + screenedCellBoundaryTerm Z R l k f x = -4 * Real.pi * nuclearFaceDensity R (↑Z) k l x * f x

theorem LiebThirring.integral_screenedCellBoundaryTerm_pair {M : ℕ} (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) (f : Position → ℝ) (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) : ∫ (x : Position) in voronoiFace R k l, screenedCellBoundaryTerm Z R k l f x ∂bisectorSurfaceMeasure R hR k l hkl + ∫ (x : Position) in voronoiFace R l k, screenedCellBoundaryTerm Z R l k f x ∂bisectorSurfaceMeasure R hR l k ⋯ = -4 * Real.pi * ∫ (x : Position) in voronoiFace R k l, nuclearFaceDensity R (↑Z) k l x * f x ∂bisectorSurfaceMeasure R hR k l hkl