laplacian_radialInv_zero_no_const_proved
plain-language theorem explainer
The theorem shows that the Laplacian of 1/r vanishes at every point where the spatial radius is nonzero. Workers discharging the C2 axioms in the Recognition Science relativity calculus cite it when converting derivative axioms into theorems. The proof applies the coordinate-wise second-derivative lemma three times, substitutes the spatial-norm identity, and closes the cancellation with field simplification plus nlinarith.
Claim. Let $r(x)$ be the Euclidean norm of the first three coordinates of the four-vector $x$. For any $x$ with $r(x) > 0$, the Laplacian of the function $1/r$ satisfies $Δ(1/r)(x) = 0$.
background
The declaration belongs to the module that replaces seven axiomatic statements in Derivatives.lean with proved theorems. Spatial radius is the square root of the sum of squares of the first three coordinates; radial inverse with exponent 1 is the reciprocal of this radius. The Laplacian operator is the sum of the three spatial second partial derivatives. The module relies on the already-proved second-derivative formula for the radial inverse and on the fact that the spatial radius is positive whenever it is nonzero.
proof idea
Unfold the Laplacian definition. Apply the second-derivative lemma for radial inverse once for each spatial coordinate index. Simplify the resulting expressions by reducing the Fin 4 equalities. Rewrite the sum using the identity between squared spatial radius and spatial norm squared. Finish with field_simp followed by nlinarith on squares and positivity of the radius to the third and fifth powers.
why it matters
The result supplies the lap_zero_holds field of the C2DischargeCert definition, which certifies that the seven axioms in Derivatives.lean are now theorems. It completes the radial-derivative segment of the C2 discharge required for the relativity calculus. In the Recognition Science chain this supports the harmonic-property step needed for potential functions that appear in observer forcing and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.