partialDeriv_v2_mul
plain-language theorem explainer
The directional derivative along coordinate rays obeys the product rule. Researchers expanding products in recognition-field Lagrangians or wave equations would cite this result. The argument unfolds the ray definition of partialDeriv_v2, invokes the ordinary deriv_mul lemma, substitutes the zero-time point via coordRay_zero, and closes with algebraic simplification.
Claim. Let $f,g: (ℝ^4 → ℝ)$, $μ ∈ Fin 4$, $x ∈ ℝ^4$. If the compositions $t ↦ f(x + t e_μ)$ and $t ↦ g(x + t e_μ)$ are differentiable at $t=0$, then $∂_μ(fg)(x) = f(x) ∂_μ g(x) + g(x) ∂_μ f(x)$, where $∂_μ h(x) := d/dt [h(x + t e_μ)]|_{t=0}$.
background
The module defines the standard basis vectors $e_μ$ and the coordinate ray coordRay $x μ t := x + t e_μ$. The directional derivative partialDeriv_v2 is the ordinary real derivative at zero of the composition $t ↦ f(coordRay x μ t)$, providing a placeholder interface for partial derivatives in the recognition scaffold (see upstream partialDeriv_v2 in Hamiltonian). The lemma coordRay_zero states that the ray evaluates to the base point $x$ at $t=0$.
proof idea
Unfold the definition of partialDeriv_v2 to expose the real derivative of the product. Apply the standard lemma deriv_mul to split the derivative of the product. Rewrite with coordRay_zero to recover the base point $x$, then close the identity by ring.
why it matters
This lemma supplies the product rule for the directional-derivative interface that supports field products in the relativity calculus. It fills a basic calculus gap before the J-uniqueness and phi-ladder steps of the forcing chain are imposed. No downstream uses are recorded yet, but the result is required for consistent differentiation in any Hamiltonian or wave-equation construction built on partialDeriv_v2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.