laplacian
plain-language theorem explainer
The laplacian definition sums the second directional derivatives along the three spatial axes for a scalar field on four-dimensional space. Researchers deriving harmonic functions or solving Poisson equations in the Recognition framework cite this when reducing the wave operator to its spatial part. The definition is a direct three-term sum of secondDeriv applications restricted to indices 1, 2, and 3.
Claim. For a scalar function $f: (Fin 4 → ℝ) → ℝ$ and point $x ∈ Fin 4 → ℝ$, the Laplacian is defined by $∇²f(x) := ∑_{i=1}^3 ∂_i² f(x)$, where each $∂_i²$ is the second partial derivative with respect to the $i$-th spatial coordinate via iterated directional derivatives.
background
In the Derivatives module the Laplacian is assembled from secondDeriv, which computes the second partial as the derivative at zero of a partialDeriv_v2 along a coordinate ray. The module works with the standard basis vectors e_μ for μ in Fin 4, restricting the sum to the three spatial directions. Upstream secondDeriv is defined by deriv (fun s => partialDeriv_v2 f μ (coordRay x ν s)) 0, placing the construction inside the four-dimensional spacetime calculus where the forcing chain fixes D = 3 spatial dimensions.
proof idea
The definition is a direct sum of three secondDeriv calls, one each for the diagonal pairs (1,1), (2,2), and (3,3). It applies the secondDeriv function from the same module to the input function f and evaluation point x, with no additional lemmas or tactics required.
why it matters
This definition supplies the spatial Laplacian used in downstream results such as laplacian_radialInv_n, which establishes ∇²(1/r^n) = n(n-1)/r^{n+2} away from the origin, and laplacian_radialInv_zero_no_const showing that 1/r is harmonic. It feeds into PvsNPMasterCert for J-cost minimization arguments in complexity assembly and into quarticRemainder_nonneg in the simplicial ledger. In the framework it realizes the D = 3 spatial structure forced by the eight-tick octave in T8, enabling reduction of the d'Alembertian to its Laplacian part.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.