partialDeriv_v2_spatialRadius
plain-language theorem explainer
The directional derivative of the spatial radius r(x) = sqrt(sum_{i=1 to 3} x_i^2) along the mu-th coordinate axis is zero for the temporal direction and equals x_mu / r(x) otherwise, when r(x) is nonzero. Relativity and radial-potential verifiers cite this to justify gradient steps in four-dimensional calculus. The proof splits on whether mu equals zero, using ray invariance plus the constant rule for the zero case and the square-root chain rule for the spatial case.
Claim. Let $r(x) = (x_1^2 + x_2^2 + x_3^2)^{1/2}$ be the spatial radius on four-vectors. For each index $mu$ in {0,1,2,3} and point $x$ with $r(x) neq 0$, the directional derivative satisfies $partial_mu r(x) = 0$ if $mu = 0$ and $partial_mu r(x) = x_mu / r(x)$ otherwise.
background
The module defines the spatial radius as the Euclidean norm on the three spatial coordinates of a four-vector and introduces coordinate rays generated by the standard basis vectors. The operator partialDeriv_v2 supplies the directional derivative along the mu-th ray at the origin. The temporal ray (mu = 0) leaves the spatial radius invariant by construction.
proof idea
Case analysis on mu = 0. The temporal case invokes the invariance lemma spatialRadius_coordRay_temporal to reduce to the constant derivative rule. The spatial case first obtains the derivative 2 x_mu of the squared norm along the ray from partialDeriv_v2_spatialNormSq, lifts it to HasDerivAt, applies the Mathlib square-root rule HasDerivAt.sqrt, and simplifies the resulting quotient by field_simp.
why it matters
This supplies the first partial of the spatial radius that is invoked by partialDeriv_v2_radialInv and secondDeriv_radialInv, which in turn discharge laplacian_radialInv_n_proved. It closes one of the seven §XXIII.B' Mathlib calculus axioms required for the relativity sector. The result supports concrete differential operators inside the Recognition framework's derivation of physics from the J-cost equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.