laplacian_smul
plain-language theorem explainer
The lemma establishes that the Laplacian operator is linear under scalar multiplication for real-valued functions on four-dimensional space. Researchers deriving wave or field equations in the Recognition Science relativity calculus would cite it when rescaling potentials or sources. The proof is a one-line wrapper that unfolds the Laplacian definition, invokes the second-derivative scalar-multiplication lemma on each spatial term, and finishes with ring simplification.
Claim. Let $f: (ℝ^4) → ℝ$ and $c ∈ ℝ$. Under the assumptions that $f$ is differentiable along every coordinate ray and that the first partial derivatives of $f$ remain differentiable along those rays, the Laplacian satisfies $∇²(cf)(x) = c ∇²f(x)$ for any $x ∈ ℝ^4$.
background
The module supplies the standard basis vectors $e_μ$ and the coordinate-ray map $x + t e_μ$ used to define directional derivatives. The directional derivative $∂_μ f(x)$ is realized as the ordinary derivative of $f$ composed with the ray at $t=0$. The Laplacian itself is the sum of the three spatial second directional derivatives (indices 1, 2, 3). The upstream lemma secondDeriv_smul already records the corresponding linearity for a single second directional derivative under the same differentiability hypotheses.
proof idea
The proof unfolds the definition of laplacian, replaces each secondDeriv term by the corresponding instance of secondDeriv_smul, and closes with the ring tactic to factor the constant $c$ out of the sum.
why it matters
This scalar-linearity result for the Laplacian supplies a basic algebraic property required by any subsequent derivation that scales fields or sources inside the relativity calculus. It sits directly above the second-derivative linearity lemma and below any application of the Laplacian to linear wave or Poisson equations in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.