deriv_add
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.
claimLet $φ_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 in Recognition Science
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.
scope and limits
- Does not establish differentiability or existence of the scalar fields.
- Does not extend to nonlinear field operations or higher-order derivatives.
- Does not replace the classical partial derivative beyond the fixed-step finite-difference approximation.
- Does not apply to vector or tensor fields.
Lean usage
rw [deriv_add]formal statement (Lean)
54theorem deriv_add (φ₁ φ₂ : ScalarField) (μ : Fin 4) (x : Fin 4 → ℝ) :
55 directional_deriv (add φ₁ φ₂) μ x =
56 directional_deriv φ₁ μ x + directional_deriv φ₂ μ x := by
proof body
Term-mode proof.
57 simp [directional_deriv, add]
58 ring
59