deriv_add_lin
The lemma establishes additivity of the directional derivative along coordinate rays in four-dimensional spacetime. Researchers modeling superposed fields in Recognition Science would cite it to justify linearity when combining solutions. The proof is a direct one-line application of the standard derivative additivity rule after unfolding the partial derivative definition.
claimLet $f, g : (ℝ^4 → ℝ)$. For each coordinate index $μ ∈ {0,1,2,3}$ and point $x ∈ ℝ^4$, if the directional restrictions $t ↦ f(γ_μ(x,t))$ and $t ↦ g(γ_μ(x,t))$ are differentiable at $t=0$, then the directional derivative of $f+g$ along the $μ$-ray at $x$ equals the sum of the individual directional derivatives.
background
The module introduces the standard basis vectors $e_μ$ in four-dimensional space and the ray parametrization coordRay that traces the line $x + t e_μ$. The function partialDeriv_v2 acts as the placeholder interface for the directional derivative of a recognition field with respect to coordinate $μ$ at point $x$; its upstream definition in the Hamiltonian module is the noncomputable constant zero, which is specialized here to differentiable scalar functions. Upstream structures supply the J-cost convexity and spectral emergence that frame the underlying field as arising from phi-forcing.
proof idea
The term proof unfolds the definition of partialDeriv_v2 and applies the exact Mathlib lemma deriv_add to the supplied differentiability hypotheses hf and hg.
why it matters in Recognition Science
This lemma supplies the basic linearity property required for derivative calculations inside the relativity calculus module. It supports superposition of fields that appear in the recognition composition law and the eight-tick octave dynamics. No downstream uses are recorded yet, but the result closes a gap in the derivative scaffold needed for the forcing chain steps T5–T8.
scope and limits
- Does not prove differentiability of the sum.
- Does not treat nonlinear combinations of fields.
- Does not incorporate a metric or curvature.
formal statement (Lean)
60lemma deriv_add_lin (f g : (Fin 4 → ℝ) → ℝ) (μ : Fin 4)
61 (x : Fin 4 → ℝ) (hf : DifferentiableAt ℝ (fun t => f (coordRay x μ t)) 0)
62 (hg : DifferentiableAt ℝ (fun t => g (coordRay x μ t)) 0) :
63 partialDeriv_v2 (fun y => f y + g y) μ x =
64 partialDeriv_v2 f μ x + partialDeriv_v2 g μ x := by
proof body
Term-mode proof.
65 unfold partialDeriv_v2
66 exact deriv_add hf hg
67
68/-- Linearity of directional derivative (scalar multiplication). -/