partialDeriv_v2_spatialNormSq
plain-language theorem explainer
The directional derivative of the squared spatial norm equals twice the coordinate component for spatial directions and vanishes in the time direction. Relativity calculus users cite this when deriving gradients of radial functions from the squared norm. The proof differentiates each squared term via component lemmas then dispatches the four index cases with fin_cases and simplification.
Claim. Let $x = (x_0, x_1, x_2, x_3)$ be coordinates in four-dimensional spacetime and let $N(x) = x_1^2 + x_2^2 + x_3^2$ be the squared spatial norm. Then the directional derivative satisfies $N_μ(x) = 0$ when $μ = 0$ and $N_μ(x) = 2 x_μ$ when $μ ∈ {1,2,3}.
background
In this module spatialNormSq is the squared Euclidean norm of the three spatial coordinates. The operator partialDeriv_v2 supplies the placeholder directional derivative interface imported from the Hamiltonian scaffold, later specialized to concrete functions. The result rests on the auxiliary lemma partialDeriv_v2_x_sq that gives the derivative of an individual squared coordinate term.
proof idea
The proof obtains the three component derivatives with partialDeriv_v2_x_sq, then applies fin_cases on μ followed by simp_all using the definitions of partialDeriv_v2, spatialNormSq, coordRay_apply, basisVec and deriv_const_add.
why it matters
The theorem supplies the derivative needed for the spatial radius in the downstream results partialDeriv_v2_spatialRadius and partialDeriv_v2_spatialRadius_proved. It completes the flat-space calculus layer required for radial quantities inside the Recognition framework, consistent with the eight-tick octave and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.