partialDeriv_v2_spatialRadius_proved
plain-language theorem explainer
The theorem establishes that the directional derivative of the spatial radius equals zero along the time axis and the normalized spatial coordinate otherwise. Researchers computing gradients for radial potentials or Laplacians in recognition-based models cite this identity to replace placeholder derivative axioms. The proof splits on the direction index, using ray invariance for the temporal case and the chain rule through the square root for spatial directions.
Claim. Let $r(x) = (x_1^2 + x_2^2 + x_3^2)^{1/2}$ denote the spatial radius of the four-vector $x$. For each index $μ ∈ {0,1,2,3}$ with $r(x) ≠ 0$, the directional derivative satisfies $∂_μ r(x) = 0$ when $μ=0$ and $∂_μ r(x) = x_μ / r(x)$ otherwise, where $∂_μ$ is realized by the partialDeriv_v2 operator.
background
spatialRadius is the Euclidean norm of the three spatial components of a four-vector, defined via the square root of spatialNormSq. partialDeriv_v2 is the directional derivative interface for recognition fields, initially introduced as a placeholder in the Hamiltonian module. The module RadialDerivativesProofs replaces seven axioms from Derivatives.lean with explicit theorems, relying on upstream lemmas such as spatialNormSq_coordRay_temporal (invariance of the spatial norm under temporal ray extensions) and partialDeriv_v2_spatialNormSq (derivative of the squared norm equals twice the coordinate).
proof idea
The tactic proof unfolds partialDeriv_v2 and spatialRadius, then cases on whether μ equals zero. The temporal branch invokes spatialNormSq_coordRay_temporal to obtain constancy along the ray and applies deriv_const. The spatial branch confirms positivity via spatialRadius_ne_zero_iff, obtains DifferentiableAt via differentiableAt_coordRay_spatialNormSq, extracts the squared-norm derivative via partialDeriv_v2_spatialNormSq, lifts to HasDerivAt, applies HasDerivAt.sqrt, and simplifies the quotient algebraically with ring_nf and norm_num.
why it matters
This identity discharges one of the C2 axioms for radial calculus and is referenced directly by c2DischargeCert, partialDeriv_v2_radialInv_proved, and secondDeriv_radialInv_proved. It supplies the concrete derivative needed for inverse-power potentials and Laplacian identities that appear in the recognition framework's three-dimensional spatial sector (T8). The result closes a scaffolding gap between the placeholder partialDeriv_v2 and downstream wave-equation or potential computations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.