directional_deriv
plain-language theorem explainer
The directional derivative definition supplies a finite-difference approximation to the partial derivative of a scalar field in one coordinate direction on 4D spacetime. Researchers building numerical or discrete models of scalar fields in relativity would cite it when establishing linearity of derivatives. The definition proceeds by a direct finite-difference formula with fixed step size 0.001.
Claim. For a scalar field given by a function $ψ : (ℝ^4) → ℝ$, the directional derivative in direction $μ ∈ {0,1,2,3}$ at point $x ∈ ℝ^4$ is defined by $(ψ(x + h e_μ) - ψ(x))/h$ where $h = 0.001$ and $e_μ$ increments only the $μ$-th coordinate.
background
A scalar field is a structure consisting of a function $ψ : (Fin 4 → ℝ) → ℝ$ that assigns a real value to each spacetime point. This definition sits inside the scalar fields module of the relativity section, where scalar fields serve as the basic objects for constructing derivatives and gradients before metric or curvature structures are introduced. The module imports Mathlib and the geometry tensor definitions; upstream dependencies are limited to interface classes such as collision-free checks and simplicial ledger constructions that do not alter the local definition.
proof idea
This is a direct definition that implements the directional derivative via a finite-difference formula. It fixes $h = 0.001$, builds the perturbed coordinate tuple by adding $h$ only to the $μ$-component, evaluates the field's $ψ$ at both points, and returns the difference quotient.
why it matters
This definition supplies the primitive operation used by the linearity theorems deriv_add, deriv_smul and deriv_constant, and by the gradient operator that collects all four directional derivatives. It therefore forms the base layer for differential calculus on scalar fields inside the Recognition Science treatment of relativity, linking to the geometry module and ultimately to the forcing chain steps that fix spatial dimension D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.