laplacian_radialInv_n
plain-language theorem explainer
Establishes that the Laplacian of 1/r^n equals n(n-1)/r^{n+2} for nonzero spatial radius in four-dimensional coordinates. Researchers deriving gravitational potentials or recognition-weighted fields would cite this identity. The proof sums the three spatial second directional derivatives via the explicit formula in secondDeriv_radialInv and finishes with algebraic reduction using r squared equals the sum of squared spatial components.
Claim. $∇²(1/r^n)(x) = n(n-1)/r^{n+2}$ where $r = √(x_1² + x_2² + x_3²) ≠ 0$, and the Laplacian is the sum of second partial derivatives over the three spatial coordinates.
background
The Laplacian is the sum of secondDeriv over spatial indices 1, 2, 3. radialInv n maps x to 1 over spatialRadius(x) to the power n and serves as the model for gravitational potentials. secondDeriv computes iterated directional derivatives along coordinate rays. The module supplies calculus primitives for the relativity section, relying on spatial geometry from the Tensor import and the explicit component formula in the upstream secondDeriv_radialInv theorem.
proof idea
Unfolds laplacian to the sum of three secondDeriv calls. Invokes secondDeriv_radialInv on each spatial diagonal pair, simplifies the conditional branches, introduces the identity spatialRadius x squared equals x1 squared plus x2 squared plus x3 squared, rewrites the power via pow_add, then applies field_simp followed by linear_combination with the coefficient -(n)(n+2) r^{n+2} times the squared-radius identity.
why it matters
Feeds the downstream laplacian_radialInv_n_proved in RadialDerivativesProofs, which restates the same identity using integer exponents. Supplies the explicit Laplacian for radial inverse potentials required by the framework's calculus axioms. Relies on the three-dimensional spatial structure from the forcing chain and closes one of the §XXIII.B′ Mathlib identities needed for potential theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.