partialDeriv_v2_x_sq
plain-language theorem explainer
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
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.