laplacian_radialInv_zero_no_const
plain-language theorem explainer
The declaration shows that the Laplacian of 1/r is identically zero at all points with nonzero spatial radius. Field theorists verifying source-free Laplace equations would cite this identity. The proof applies the second-derivative formula coordinatewise for the three spatial directions and reduces the resulting sum to zero by algebraic cancellation using the squared-radius identity.
Claim. Let $r$ denote the spatial radius on four-dimensional space. For any point $x$ with $r(x) ≠ 0$, the Laplacian of the map $y ↦ 1/r(y)$ evaluated at $x$ equals zero.
background
The Derivatives module defines the Laplacian as the sum of second partial derivatives along the three spatial coordinates of a four-dimensional point, using the standard basis for projections. The radial inverse of order one is the reciprocal of this spatial radius, where the radius is the Euclidean norm of the first three coordinates. The module setting centers on coordinate calculus for relativistic field operators.
proof idea
The proof unfolds the Laplacian definition and invokes the positivity lemma for the spatial radius. It applies the second-derivative formula for the radial inverse three times, once per spatial index. After index normalization it substitutes the squared-radius identity and finishes with field simplification followed by the ring tactic.
why it matters
This supplies the n=1 base case for the general Laplacian formula of 1/r^n in the RadialDerivativesProofs module. The doc-comment positions the result as closing one of the Mathlib calculus axioms in §XXIII.B′. In the Recognition framework it confirms the harmonic property of the Coulomb potential in the three spatial dimensions forced by the unified chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.