sq_le_spatialNormSq_1
plain-language theorem explainer
The inequality asserts that the square of the first spatial coordinate of any four-vector is bounded above by the squared spatial norm. It is invoked in arguments showing that spatial radius remains positive after small coordinate perturbations along basis directions. The proof is a one-line wrapper that unfolds the spatial norm definition and invokes non-linear arithmetic on the non-negative squares of the remaining spatial components.
Claim. For any $x : Fin 4 → ℝ$, $x_1^2 ≤ x_1^2 + x_2^2 + x_3^2$.
background
The spatial norm squared is defined as the sum of squares of the three spatial components of a four-vector in Minkowski space. This lemma sits inside the Derivatives submodule of the Relativity calculus, which works with coordinate representations and partial derivatives built on the tensor geometry import. The upstream definition supplies the exact expression that the inequality compares against.
proof idea
One-line wrapper that unfolds spatialNormSq and applies nlinarith to the non-negativity of the squares of the second and third components.
why it matters
It supplies the concrete bound needed inside the proof of spatialRadius_coordRay_ne_zero, which guarantees that spatial radius stays nonzero under sufficiently small shifts along any coordinate direction. This step supports stable coordinate-ray constructions used in derivative calculations within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.