partialDeriv_v2_x_sq
The theorem supplies the explicit evaluation of the partial derivative interface applied to the squared i-th coordinate function, yielding twice the coordinate value times the Kronecker delta at the differentiation index. Workers deriving spatial norm gradients or relativistic field equations cite it to simplify sums of squared coordinates. The proof unfolds the placeholder derivative, introduces a linear ray along the basis vector, invokes the power rule at a differentiable point, and reduces the two index cases with basis-vector identities, a
claimFor indices $i, mu in {0,1,2,3}$ and point $x in R^4$, the partial derivative interface satisfies $partial_mu (x_i^2) = 2 x_i delta_{i mu}$, where $delta$ is the Kronecker symbol that equals 1 precisely when the indices coincide.
background
The module introduces the standard basis vector $e_mu$ that equals 1 at index $mu$ and 0 elsewhere. The partial derivative interface partialDeriv_v2 is a non-computable placeholder returning a real scalar for any input function, direction index, and evaluation point; it is intended to stand in for the recognition-field derivative scaffold. Upstream arithmetic lemmas supply the ring identities add_zero, mul_one and mul_zero that close the algebraic simplifications once the derivative rules are applied.
proof idea
Unfold the placeholder definition and simplify the coordinate-ray applicator. Define the auxiliary ray function f_i(t) = x_i + t * e_mu(i), record its differentiability at zero, rewrite the squared term as f_i squared, apply the power rule for the second derivative, then case-split on whether i equals mu. When indices match, substitute the self-value of the basis vector, differentiate the constant-plus-identity expression, and ring; when they differ, substitute the zero value, differentiate the constant, and ring.
why it matters in Recognition Science
The result is invoked by partialDeriv_v2_spatialNormSq to obtain the functional derivative of the sum of squared spatial coordinates, which equals twice the mu-component for spatial directions and zero for the time direction. It supplies the concrete calculus step required to connect the placeholder derivative interface to the Recognition Composition Law and the eight-tick octave structure, thereby supporting explicit computations on the phi-ladder. No open scaffolding remains at this node.
scope and limits
- Does not compute derivatives of non-quadratic or non-polynomial functions.
- Does not incorporate a metric tensor or curvature corrections.
- Does not address time-component special cases beyond the Kronecker factor.
- Does not extend to higher-order or distributional derivatives.
Lean usage
have hd1 := partialDeriv_v2_x_sq mu 1 xformal statement (Lean)
365theorem partialDeriv_v2_x_sq (μ i : Fin 4) (x : Fin 4 → ℝ) :
366 partialDeriv_v2 (fun y => y i ^ 2) μ x = 2 * x i * (if i = μ then 1 else 0) := by
proof body
Term-mode proof.
367 unfold partialDeriv_v2
368 simp only [coordRay_apply]
369 let f_i := fun t => x i + t * basisVec μ i
370 have h_f : DifferentiableAt ℝ f_i 0 := differentiableAt_coordRay_i x μ i
371 rw [show (fun t => (x i + t * basisVec μ i) ^ 2) = f_i ^ 2 by rfl]
372 rw [deriv_pow h_f 2]
373 simp only [f_i]
374 split_ifs with h_eq
375 · subst h_eq
376 simp only [basisVec_self, mul_one]
377 rw [deriv_const_add, deriv_id'']
378 ring
379 · simp only [basisVec_ne h_eq, mul_zero, add_zero]
380 rw [deriv_const]
381 ring
382