partialDeriv_v2
plain-language theorem explainer
partialDeriv_v2 defines the directional derivative of a scalar function f at x along the μ-th coordinate by restricting f to the coordinate ray and taking the ordinary real derivative at t=0. Physicists constructing Hamiltonian densities or stress-energy tensors from the recognition field cite this operator. It is realized as a direct one-line wrapper around the real derivative applied to the ray restriction.
Claim. The directional derivative is defined by $∂_μ f(x) := d/dt|_{t=0} f(coordRay(x, μ, t))$, where coordRay parametrizes the straight line through x in the direction of the μ-th standard basis vector of ℝ⁴.
background
The Derivatives module equips Minkowski space with the standard basis vectors e_μ and the coordinate ray coordRay x μ t that shifts x by t along the μ direction. This supplies the concrete calculus layer for field derivatives. It replaces the placeholder partialDeriv_v2 from the Hamiltonian module and is presupposed by linearity results such as deriv_add_lin.
proof idea
The definition is a one-line wrapper that applies the real derivative operator to the restriction t ↦ f(coordRay x μ t) evaluated at zero.
why it matters
This definition supplies the partial derivative appearing inside HamiltonianDensity and StressEnergyTensor, where it enters quadratic terms such as (partialDeriv_v2 psi 0 x)². It completes the relativity calculus interface that feeds the recognition Hamiltonian and stress-energy constructions, linking to the J-cost structures and phi-ladder upstream in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.