secondDeriv_smul
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of any derivatives.
- Does not extend to vector-valued or tensor-valued functions.
- Does not address derivatives of order higher than two.
- Does not incorporate metric factors or curvature corrections.
Lean usage
simp only [secondDeriv_smul f c _ _ x (h1 _) (h2 _ _)]formal statement (Lean)
92lemma secondDeriv_smul (f : (Fin 4 → ℝ) → ℝ) (c : ℝ) (μ ν : Fin 4)
93 (x : Fin 4 → ℝ)
94 (h1 : ∀ y, DifferentiableAt ℝ (fun t => f (coordRay y μ t)) 0)
95 (h2 : DifferentiableAt ℝ (fun s => partialDeriv_v2 f μ (coordRay x ν s)) 0) :
96 secondDeriv (fun y => c * f y) μ ν x = c * secondDeriv f μ ν x := by
proof body
Tactic-mode proof.
97 unfold secondDeriv
98 have h_partial : ∀ y, partialDeriv_v2 (fun z => c * f z) μ y = c * partialDeriv_v2 f μ y := by
99 intro y
100 exact partialDeriv_v2_smul f c μ y (h1 y)
101 simp only [h_partial]
102 exact deriv_const_mul c h2
103
104/-- Laplacian linearity (scalar multiplication). -/