secondDeriv_smul
plain-language theorem explainer
The lemma establishes linearity of the second directional derivative under scalar multiplication of the function. Researchers building differential operators for relativistic wave equations would cite it to confirm that scaling a field preserves the form of second-order terms. The proof unfolds the iterated derivative definition, reduces the inner first derivative via its own linearity result, and finishes with the constant-multiple differentiation rule.
Claim. Let $f: (Fin 4 → ℝ) → ℝ$, $c ∈ ℝ$, and indices $μ, ν ∈ Fin 4$. Under the assumptions that the directional derivative of $f$ along the $μ$-ray exists at every point and the directional derivative of the $μ$-partial along the $ν$-ray exists at $x$, the second directional derivative satisfies $∂_μ ∂_ν (c f)(x) = c ⋅ ∂_μ ∂_ν f(x)$, where each partial is the ordinary derivative at zero along the appropriate coordinate ray.
background
The module supplies coordinate calculus on ℝ⁴ using the standard basis vectors $e_μ$. A coordinate ray is the line $x + t e_μ$. The first directional derivative $∂_μ f(x)$ is defined as the ordinary derivative at $t=0$ of $f$ composed with this ray. The second derivative $∂_μ ∂_ν f(x)$ iterates the construction by differentiating the $μ$-partial along the $ν$-ray. Upstream partialDeriv_v2_smul records the identical linearity statement at first order: “Linearity of directional derivative (scalar multiplication).”
proof idea
The tactic proof unfolds the definition of secondDeriv. It introduces an auxiliary fact that the inner partial derivative of the scaled function equals the scaled partial, obtained directly by applying partialDeriv_v2_smul to the supplied differentiability hypothesis. After simplification the goal reduces to the derivative of a constant multiple, which is discharged by deriv_const_mul.
why it matters
The result supplies the scalar-multiplication case needed to prove the same linearity for the Laplacian, which is the immediate downstream consumer. It therefore closes the algebraic properties of the second-order operators in the relativity calculus layer. Within the Recognition framework this supports consistent scaling of field equations without introducing extra terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.