spatialRadius_ne_zero_iff
plain-language theorem explainer
The equivalence between nonzero spatial radius and nonzero spatial norm squared for four-vectors is used in differentiability arguments for radial functions along coordinate rays. Researchers deriving partial derivatives in Minkowski space cite it to pass between radius and norm conditions. The proof is a one-line wrapper that unfolds the square-root definition and applies the real square-root non-zero lemma to the nonnegativity of the squared norm.
Claim. For a four-vector $x = (x_0, x_1, x_2, x_3) : Fin 4 → ℝ$, let $r(x) := √(x_1² + x_2² + x_3²)$. Then $r(x) ≠ 0$ if and only if $x_1² + x_2² + x_3² ≠ 0$.
background
In the Derivatives module, spatialNormSq is the squared Euclidean norm of the three spatial components of a four-vector, defined as x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2. spatialRadius is the corresponding positive square root, so the two quantities vanish together. The module works in the standard Minkowski setting with coordinate rays generated by basis vectors e_μ and imports the Tensor geometry layer. Upstream, spatialNormSq_nonneg supplies the nonnegativity needed to guarantee the square root is real-valued and the equivalence holds.
proof idea
One-line wrapper. Unfold the definition of spatialRadius, then rewrite with Real.sqrt_ne_zero applied to the hypothesis spatialNormSq_nonneg x.
why it matters
The result is invoked directly in downstream theorems including differentiableAt_coordRay_spatialRadius, partialDeriv_v2_spatialRadius, and spatialRadius_coordRay_ne_zero to discharge non-zero hypotheses before applying chain-rule or division steps. It supplies a basic algebraic link in the radial calculus that supports the Recognition Science forcing chain at T8 (D = 3 spatial dimensions) and the construction of well-defined radial derivatives on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.