Directed boundary expression for the nearest-nucleus deficit

The nearest-distance factor turns outward inverse-cubic flux into inverse-fourth flux.

The half nearest-charge integral has exactly the Z²/(8π) directed coefficient.

theorem LiebThirring.nearestKernel_mul_faceFlux {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l : Fin M} {y : Position} (hy : y ∈ voronoiFace R k l) : (nearestNucleusDistance R y)⁻¹ * ENNReal.ofReal (nuclearFaceFlux R k l y) = ENNReal.ofReal (nuclearHalfDistance R k l / ‖y - R k‖ ^ 4)

The nearest-distance factor turns outward inverse-cubic flux into inverse-fourth flux.

theorem LiebThirring.half_nearestIntegral_eq_directed_inverse_fourth {M : ℕ} (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) : (∫⁻ (y : Position), ↑Z * (nearestNucleusDistance R y)⁻¹ ∂voronoiFaceMeasure R hR ↑Z) / 2 = ENNReal.ofReal (↑Z ^ 2 / (8 * Real.pi)) * ∑ k : Fin M, ∑ l : { l : Fin M // l ≠ k }, ∫⁻ (y : Position) in voronoiFace R k ↑l, ENNReal.ofReal (nuclearHalfDistance R k ↑l / ‖y - R k‖ ^ 4) ∂bisectorSurfaceMeasure R hR k ↑l ⋯

The half nearest-charge integral has exactly the Z²/(8π) directed coefficient.

theorem LiebThirring.half_energy_add_directed_boundary_eq_repulsion_of_potential_eq {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (hPhi : ∀ (x : Position), screenedPotential Z R x = coulombPotential (voronoiFaceMeasure R hR ↑Z) x) : coulombEnergy (voronoiFaceMeasure R hR ↑Z) (voronoiFaceMeasure R hR ↑Z) / 2 + ENNReal.ofReal (↑Z ^ 2 / (8 * Real.pi)) * ∑ k : Fin M, ∑ l : { l : Fin M // l ≠ k }, ∫⁻ (y : Position) in voronoiFace R k ↑l, ENNReal.ofReal (nuclearHalfDistance R k ↑l / ‖y - R k‖ ^ 4) ∂bisectorSurfaceMeasure R hR k ↑l ⋯ = nuclearRepulsion (fun (x : Fin M) => Z) R

Exact energy normalization with the directed boundary integral, conditional only on the potential identity.