spatialNormSq_coordRay_spatial_2
plain-language theorem explainer
The lemma computes the squared spatial norm after shifting the second spatial coordinate of a four-vector by an arbitrary real parameter s. Analysts deriving coordinate derivatives or verifying radius bounds in relativistic settings cite this identity when handling perturbations along individual spatial axes. The proof is a direct term-mode reduction that unfolds the three core definitions, resolves the index cases for the second basis vector, and simplifies the resulting expression by ring arithmetic.
Claim. Let $x : (Fin 4) → ℝ$ and $s ∈ ℝ$. The squared spatial norm of the perturbed vector $x + s · e_2$, where $e_2$ is the standard basis vector with 1 in the second spatial slot, equals $x_1^2 + (x_2 + s)^2 + x_3^2$.
background
In this module the spatial norm squared is defined as the sum of squares of the three spatial components: spatialNormSq(x) := x 1² + x 2² + x 3². The coordinate ray operator adds a multiple of a chosen basis vector: coordRay(x, μ, t) returns the function ν ↦ x ν + t · basisVec(μ, ν). The basis vector itself is the standard Kronecker delta: basisVec(μ, ν) = 1 if ν = μ and 0 otherwise. These three definitions together encode the action of shifting a four-vector along one of the four coordinate directions while leaving the others fixed. The module imports the tensor geometry layer and works throughout in the standard Minkowski signature with indices 0 (time) and 1,2,3 (space).
proof idea
The term proof first unfolds spatialNormSq, coordRay and basisVec. It then rewrites the resulting expression by replacing the three relevant if-expressions: the index-1 case is false, the index-2 case is true, and the index-3 case is false. The final ring tactic collapses the arithmetic to the claimed sum of squares.
why it matters
This identity is invoked inside the proof of spatialRadius_coordRay_ne_zero, which establishes that a sufficiently small shift along any coordinate direction preserves a nonzero spatial radius. The result therefore supplies one of the concrete algebraic steps needed to control perturbations in the relativistic calculus layer. Within the Recognition Science framework it aligns with the fixed choice of three spatial dimensions (T8) and supports the derivative constructions that ultimately feed into the forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.