partialDeriv_v2_const
plain-language theorem explainer
If a scalar field f on R^4 is identically equal to a constant c, its directional derivative along any coordinate axis vanishes at every point. Curvature calculations in flat spacetime cite this to conclude that the Minkowski metric has zero derivatives and that the Riemann tensor is identically zero. The short tactic proof unfolds the ray definition of the directional derivative, substitutes the constant value, and invokes the standard fact that the real derivative of a constant function is zero.
Claim. Let $f: (Fin 4 → ℝ) → ℝ$ and $c ∈ ℝ$. If $f(y) = c$ for every $y$, then the directional derivative $∂_μ f(x) := d/dt|_{t=0} f(x + t e_μ)$ equals zero for every coordinate index $μ$ and every point $x$.
background
The module supplies the coordinate ray $coordRay x μ t := x + t · e_μ$ where $e_μ$ is the standard basis vector in four dimensions. The directional derivative $partialDeriv_v2 f μ x$ is defined as the ordinary derivative at $t=0$ of the composite $f ∘ coordRay x μ$. The upstream placeholder $partialDeriv_v2$ in the Hamiltonian module is replaced here by this concrete ray construction, allowing direct appeal to real-analysis facts about derivatives.
proof idea
Unfold the definition of $partialDeriv_v2$ to expose the real derivative along the ray. Construct an auxiliary equality showing that the pulled-back function is the constant function with value $c$. Rewrite with this equality and finish with the library lemma $deriv_const$.
why it matters
The lemma is invoked directly by $eta_deriv_zero$ to show that the Minkowski metric is independent of position, and by $minkowski_riemann_zero$ to conclude that the Riemann tensor vanishes identically in flat space. It therefore closes the step from the recognition-forced flat metric to the vanishing of curvature tensors required for the Minkowski background in the relativity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.