spatialRadius_coordRay_ne_zero
plain-language theorem explainer
The spatial radius of a four-vector stays nonzero after a coordinate shift of size less than half the original radius. Analysts deriving radial derivatives and Laplacians in Minkowski space cite this to keep the norm positive during differentiation. The proof rewrites via the norm-zero equivalence, splits on direction index, and reaches a contradiction with the size bound for each spatial case using norm inequalities and linear arithmetic.
Claim. Let $r(x) = (x_1^2 + x_2^2 + x_3^2)^{1/2}$. If $r(x) > 0$ and $|s| < r(x)/2$, then the vector $x + s e_ν$ satisfies $r(x + s e_ν) > 0$ for every coordinate index $ν$.
background
spatialRadius extracts the Euclidean length of the three spatial components of a four-vector. coordRay adds a signed increment $s$ along one standard basis direction $e_ν$. The module supplies differentiation rules for radial functions on Minkowski space, assuming the spatial norm squared equals the sum of squares on indices 1, 2, 3 and the standard basis vectors from the tensor geometry import.
proof idea
The tactic proof first rewrites the goal with spatialRadius_ne_zero_iff and records positivity of the input radius. It then obtains the underlying natural number of $ν$ and matches on the four cases. The temporal case reduces directly to the input hypothesis. Each spatial case assumes the perturbed norm vanishes, applies nlinarith to force the unshifted components to zero and the shifted one to $-s$, derives that the original radius equals $|s|$, and obtains the contradiction with the hypothesis via linarith.
why it matters
The result is invoked by laplacian_radialInv_n_proved to justify the Laplacian formula for $1/r^n$. It closes one of the calculus axioms listed in the module documentation for radial derivatives. Within the Recognition framework it supplies the local non-vanishing needed for differentiation away from the spatial origin in the three-dimensional spatial sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.