spatialRadius_pos_of_ne_zero
plain-language theorem explainer
If the spatial radius of a four-vector is nonzero then it is positive. Researchers deriving Laplacian identities for radial inverses and directional derivatives cite it to justify positivity when the radius is assumed nonzero. The proof reduces the claim to nonnegativity of the squared spatial norm via two equivalence lemmas and an order fact.
Claim. Let $r(x) = (x_1^2 + x_2^2 + x_3^2)^{1/2}$ for $x$ in four-dimensional real space. If $r(x) ≠ 0$ then $r(x) > 0$.
background
Spatial norm squared sums the squares of the three spatial coordinates of the input four-vector. Spatial radius is the square root of that sum and is nonnegative by definition. The Derivatives module builds operators for radial functions and their derivatives in spacetime calculus, relying on the nonnegativity theorem for the squared norm together with equivalences that link the radius being nonzero or positive to the same properties of the squared norm.
proof idea
The argument applies the equivalence lemma converting nonzero radius into nonzero squared norm. It then invokes the positivity equivalence for the square root, feeding in the nonnegativity of the squared norm and the fact that it differs from zero, to obtain the strict inequality via the order lemma lt_of_le_of_ne.
why it matters
The result is invoked directly in the statements of laplacian_radialInv_n, laplacian_radialInv_zero_no_const, partialDeriv_v2_radialInv and secondDeriv_radialInv to guarantee positivity away from the origin. These close the remaining Mathlib calculus axioms for radial inverses. It supports the three-dimensional spatial geometry by ensuring radial expressions remain positive whenever nonzero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.