spatialNormSq_nonneg
plain-language theorem explainer
The declaration establishes nonnegativity of the squared spatial norm for any real four-vector. Researchers deriving radial Laplacians or coordinate derivatives in special relativity cite it to guarantee positivity when taking square roots or applying inequalities. The proof is a one-line wrapper that unfolds the definition and invokes the positivity tactic.
Claim. For any real vector $x = (x_0, x_1, x_2, x_3)$, the sum of squares of its spatial components satisfies $x_1^2 + x_2^2 + x_3^2 ≥ 0$.
background
The spatial norm squared is defined explicitly as the sum of squares of the three spatial coordinates: $x_1^2 + x_2^2 + x_3^2$. This definition sits inside the module on calculus derivatives for Minkowski space, where coordinates are indexed by Fin 4 with index 0 temporal and indices 1-3 spatial. The surrounding context supplies standard basis vectors and coordinate rays for directional derivatives.
proof idea
The proof unfolds the definition of spatialNormSq to expose the explicit sum of three squares, then applies the positivity tactic which recognizes that each square is nonnegative and their sum inherits the property.
why it matters
This result is invoked by eleven downstream theorems, including spatialRadius_ne_zero_iff (which rewrites nonzero radius via the norm squared), laplacian_radialInv_n (which uses positivity to close the harmonic property away from the origin), and partialDeriv_v2_spatialRadius. It supplies the nonnegativity axiom needed for square-root definitions and radial calculus in three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.