partialDeriv_v2_smul
plain-language theorem explainer
The lemma establishes linearity of the partial derivative operator under scalar multiplication for functions on four-dimensional space. Researchers working on relativistic field equations in the Recognition Science framework would cite it when scaling recognition fields. The proof reduces directly to the standard derivative rule for constant multiples after unfolding the definition of partialDeriv_v2.
Claim. Let $f: (Fin 4 → ℝ) → ℝ$, $c ∈ ℝ$, $μ ∈ Fin 4$, and $x ∈ Fin 4 → ℝ$. If $f$ is differentiable at the origin along the coordinate ray in direction $μ$ from $x$, then the directional partial derivative satisfies $∂_μ (c · f)(x) = c · ∂_μ f(x)$, where $∂_μ$ denotes the operator defined via the ray parametrization.
background
The module sets the local context around the standard basis vector $e_μ$ in four-dimensional space. partialDeriv_v2 acts as the placeholder interface for the partial derivative of a recognition field in direction $μ$ at point $x$, returning zero in its base definition but serving as the scaffold for calculus operations. The differentiability hypothesis is expressed using coordRay, which parametrizes the line through $x$ along the $μ$-th coordinate axis. Upstream, the definition of partialDeriv_v2 originates in the Hamiltonian module as a noncomputable placeholder for recognition-field derivatives.
proof idea
The proof is a one-line wrapper that unfolds partialDeriv_v2 to expose the underlying derivative and then applies the exact Mathlib lemma deriv_const_mul c hf, which directly yields the constant-multiple rule under the supplied differentiability assumption.
why it matters
This result feeds directly into the second-derivative lemmas secondDeriv_smul and secondDeriv_smul_local in the same module, supplying the scalar-multiplication step required to build higher-order calculus for recognition fields. It supports the relativistic derivative layer that sits above the Hamiltonian placeholder and aligns with the broader Recognition Science forcing chain by enabling consistent scaling of field quantities. No open scaffolding questions are closed by this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.