sq_le_spatialNormSq_2
plain-language theorem explainer
The lemma asserts that for any real four-vector x the square of its second coordinate is at most the sum of the squares of its three spatial coordinates. It is cited inside proofs that control spatial radius under small coordinate shifts. The argument is a one-line wrapper that unfolds the spatial-norm definition and feeds non-negativity of the remaining squares to nlinarith.
Claim. For any $x : Fin 4 → ℝ$, $x_2^2 ≤ x_1^2 + x_2^2 + x_3^2$.
background
Vectors in this module are maps from Fin 4 to ℝ, with index 0 reserved for the time coordinate and indices 1, 2, 3 for the three spatial directions. The auxiliary definition spatialNormSq expands to the sum of squares of those three spatial entries. The surrounding calculus layer supplies coordinate-ray perturbations and radius functions that rely on elementary comparisons between individual squared components and the full spatial sum.
proof idea
One-line wrapper. The tactic first unfolds spatialNormSq, exposing the explicit sum of three squares, then invokes nlinarith on the two non-negative squares (x 1)^2 and (x 3)^2 to conclude the desired inequality.
why it matters
The result is invoked directly by spatialRadius_coordRay_ne_zero, which shows that sufficiently small shifts along any coordinate axis leave the spatial radius nonzero. It therefore supplies a quantitative ingredient for the perturbation arguments that keep spatial-radius expressions well-defined inside the relativity calculus. No link to the core T0–T8 forcing chain appears; the lemma remains a local technical bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.