gradient
plain-language theorem explainer
The gradient assembles the four directional derivatives of a scalar field φ into a vector at each spacetime point x. Researchers working on relativistic scalar fields or discrete potential functions cite it to express gradients explicitly in four-dimensional spacetime. The definition is a one-line wrapper that applies the directional derivative operator componentwise.
Claim. The gradient of scalar field φ at spacetime point x ∈ ℝ⁴ is the vector whose μ-component is the directional derivative ∂_μ φ(x) for each coordinate direction μ = 0,…,3.
background
A scalar field assigns a real value to each point in four-dimensional spacetime via a map ψ : (ℝ⁴) → ℝ. The directional derivative in direction μ is computed by a finite-difference quotient with step size 0.001 along the μ-axis while holding other coordinates fixed. This definition lives in the relativity module that equips spacetime with Fin 4 indexing and treats scalar fields as the basic objects for later gradient-based constructions.
proof idea
The definition is a one-line wrapper that applies directional_deriv to each index μ.
why it matters
This definition supplies the gradient operator required by potential-function structures in ledger algebra and by geodesic-equation checks in the action module. It supports downstream claims that edge weights equal potential differences and that constant paths are geodesics. In the Recognition Science setting it furnishes the explicit gradient needed for J-cost landscapes and exactness arguments on discrete graphs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.