sq_le_spatialNormSq_3
plain-language theorem explainer
The lemma establishes that the square of the third coordinate of any 4-vector is bounded above by its squared spatial Euclidean norm. It is invoked in coordinate perturbation arguments within relativistic derivative calculations. The proof is a direct one-line algebraic reduction that unfolds the norm definition and applies nonnegativity of squares on the remaining spatial components.
Claim. For any $x : (Fin 4) → ℝ$, let $||x||_{spatial}^2 := x_1^2 + x_2^2 + x_3^2$. Then $x_3^2 ≤ ||x||_{spatial}^2$.
background
In the Relativity.Calculus.Derivatives module the spatial norm is the Euclidean squared length on the three spatial coordinates of a 4-vector (index 0 reserved for time). This definition supports radius functions and derivative operators in a fixed coordinate chart. The module works with the standard basis vectors $e_μ$ to express directional perturbations such as coordRay.
proof idea
One-line term-mode wrapper: unfold spatialNormSq then apply nlinarith to the nonnegativity of squares on the first and second components.
why it matters
The result is used by spatialRadius_coordRay_ne_zero to guarantee that small shifts along any spatial direction keep the spatial radius nonzero. It supplies an elementary bound required for the derivative calculus that underpins the Recognition Science treatment of relativistic quantities, consistent with the D = 3 spatial dimensions forced by the T8 step of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.