spatialNormSq_coordRay_spatial_3
plain-language theorem explainer
The lemma states that for any 4-vector x and scalar s the squared spatial norm after adding s times the third basis vector equals the sum of the squares of the first two components plus the square of the shifted third component. Workers deriving coordinate perturbations or radius bounds in Recognition Science relativity cite it when specializing the general ray construction to one spatial direction. The proof is a direct term reduction that unfolds the norm and ray definitions, selects the matching index case via conditional rewrites, and rings
Claim. For any vector $x : (0,1,2,3) → ℝ$ and scalar $s ∈ ℝ$, the squared Euclidean norm on the spatial components of the perturbed vector $x + s · e_3$ equals $x_1^2 + x_2^2 + (x_3 + s)^2$.
background
The module defines the standard basis vector $e_μ$ for $μ = 0,1,2,3$ and the coordinate-ray map that adds a multiple of one basis vector to a given 4-vector. Spatial norm squared extracts the sum of squares over the three spatial slots (indices 1,2,3). This lemma is the explicit expansion for the case of the third spatial direction. The surrounding calculus layer supplies the operations needed for derivatives and radii on 4-vectors in the 3+1 setting. Upstream structures supply the J-cost and ledger factorization used elsewhere in the module, while the immediate dependencies are the basis and ray definitions themselves.
proof idea
Term-mode proof: unfold spatialNormSq, coordRay and basisVec, then rewrite with the three conditional statements that pick the positive case only for index 3 and the negative cases for indices 1 and 2, and finish with ring.
why it matters
The lemma is invoked inside the proof of spatialRadius_coordRay_ne_zero, the quantitative statement that spatial radius stays positive under small perturbations in any direction. It supplies the explicit algebraic identity required for the ν = 3 case in the case-split described in that theorem’s doc comment. The result therefore closes one concrete instance of the §XXIII.B′ calculus axioms and supports the overall 3+1-dimensional derivative machinery consistent with the forced D = 3 from the T8 step of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.