deriv_add
plain-language theorem explainer
Directional derivative distributes over addition of scalar fields. Researchers modeling weak-field superpositions or running gravitational constants cite this result to justify linear combinations. The proof is a one-line wrapper that unfolds the finite-difference definition and applies ring simplification.
Claim. Let $φ_1, φ_2$ be scalar fields on spacetime, $μ ∈ Fin 4$, and $x : Fin 4 → ℝ$. Then the directional derivative of the sum $φ_1 + φ_2$ in direction $μ$ at $x$ equals the sum of the individual directional derivatives: $∂_μ(φ_1 + φ_2)(x) = ∂_μ φ_1(x) + ∂_μ φ_2(x)$.
background
A scalar field assigns a real value to each spacetime point via the structure ScalarField with component ψ : (Fin 4 → ℝ) → ℝ. The directional derivative in direction μ at x is the finite-difference quotient (ψ(x + h e_μ) − ψ(x))/h with fixed step h = 0.001. Addition of scalar fields is defined pointwise. The module sets the local setting for scalar fields in relativity and imports the directional_deriv definition together with the geometry-level ScalarField abbreviation.
proof idea
The proof is a one-line wrapper that applies simp on the directional_deriv and add definitions, followed by ring to confirm the finite differences add linearly.
why it matters
This result feeds gradient_superposition (weak-field superposition theorem) and running_g_scaling (nanoscale G strengthening). It supplies the linearity step required for ODE diagonalization in cost functionals and growth ODEs. The declaration closes the basic additivity needed for the Recognition framework's scalar-field treatment in relativity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.