secondDeriv_smul_local
The lemma establishes that second directional derivatives commute with scalar multiplication for real functions on R^4 under local differentiability along coordinate rays. Researchers deriving wave operators or scaled potentials in relativistic field theory would cite it to justify linearity when multiplying sources by constants. The proof unfolds the iterated derivative definition, transfers the scalar through the inner partial via an eventually-equal filter, and finishes with the constant-multiplication rule for the outer derivative.
claimLet $f: (Fin 4 → ℝ) → ℝ$, $c ∈ ℝ$, $μ,ν ∈ Fin 4$, $x ∈ Fin 4 → ℝ$. Under the assumptions that $t ↦ f(coordRay(x,ν,t))$ is differentiable at 0 in a neighborhood of 0 and that the directional derivative in direction $μ$ is differentiable at 0 along the ray in direction $ν$, the second directional derivative satisfies $∂_μ ∂_ν (c f)(x) = c ⋅ ∂_μ ∂_ν f(x)$, where both derivatives are realized as ordinary derivatives along coordinate rays.
background
The Derivatives module equips 4D spacetime with directional calculus via coordinate rays. coordRay(x, μ, t) returns the point x + t ⋅ e_μ, where e_μ is the standard basis vector in Fin 4. partialDeriv_v2(f, μ, x) is defined as the ordinary derivative at t=0 of f along this ray. secondDeriv(f, μ, ν, x) iterates the construction by taking the μ-directional derivative of the function obtained by displacing x along the ν-ray. The upstream partialDeriv_v2_smul lemma already records the corresponding first-order linearity under pointwise differentiability; the present result lifts it to second order while weakening the hypothesis to a neighborhood filter.
proof idea
Unfold secondDeriv to expose the outer derivative of the μ-partial. Apply h1.mono together with partialDeriv_v2_smul to obtain an eventually-equal statement that the scaled inner partial equals c times the original partial. Invoke Filter.EventuallyEq.deriv_eq to interchange the constant with the outer derivative. Conclude with deriv_const_mul applied to h2.
why it matters in Recognition Science
The result supplies the local scalar-multiplication rule needed for linearity of second-order operators in relativistic calculus. It rests directly on partialDeriv_v2_smul and the ray-based definitions of partialDeriv_v2 and secondDeriv. Within Recognition Science it supports consistent scaling of fields when constructing the d'Alembertian or Hamiltonian structures on 4D spacetime (Fin 4), consistent with the eight-tick octave and the emergence of D=3 spatial dimensions. No downstream uses are recorded, indicating it functions as an internal lemma for tensor or field-equation derivations.
scope and limits
- Does not establish any differentiability; only assumes the stated local conditions.
- Does not extend to non-constant scalar fields or position-dependent multipliers.
- Does not apply to vector- or tensor-valued functions.
- Does not treat higher-order derivatives or mixed partials beyond the given indices.
- Does not address weak or distributional derivatives.
formal statement (Lean)
77lemma secondDeriv_smul_local (f : (Fin 4 → ℝ) → ℝ) (c : ℝ) (μ ν : Fin 4)
78 (x : Fin 4 → ℝ)
79 (h1 : ∀ᶠ s in 𝓝 0, DifferentiableAt ℝ (fun t => f (coordRay (coordRay x ν s) μ t)) 0)
80 (h2 : DifferentiableAt ℝ (fun s => partialDeriv_v2 f μ (coordRay x ν s)) 0) :
81 secondDeriv (fun y => c * f y) μ ν x = c * secondDeriv f μ ν x := by
proof body
Tactic-mode proof.
82 unfold secondDeriv
83 have h_ev : ∀ᶠ s in 𝓝 0, partialDeriv_v2 (fun z => c * f z) μ (coordRay x ν s) =
84 c * partialDeriv_v2 f μ (coordRay x ν s) := by
85 apply h1.mono
86 intro s hs
87 exact partialDeriv_v2_smul f c μ (coordRay x ν s) hs
88 rw [Filter.EventuallyEq.deriv_eq h_ev]
89 exact deriv_const_mul c h2
90
91/-- Second derivative linearity (scalar multiplication). -/