spatialNormSq
plain-language theorem explainer
The definition introduces the squared Euclidean norm on the three spatial coordinates of a four-vector x. Researchers deriving radial derivatives or the Laplacian of 1/r in relativistic settings cite it as the primitive for spatial calculus. The implementation is a direct sum of squares with no lemmas or tactics applied.
Claim. For a vector $x : {R}^4$, the spatial norm squared is defined by $x_1^2 + x_2^2 + x_3^2$.
background
The module sets up standard basis vectors $e_μ$ and coordinate rays for relativistic derivative calculations. Spatial norm squared extracts the Euclidean squared length from the spatial subspace (indices 1, 2, 3), excluding the temporal component at index 0. It is the direct input to spatial radius and to all partial derivative and Laplacian identities that follow.
proof idea
Direct definition: spatialNormSq x := x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2. No upstream lemmas or tactics are invoked; the expression is the primitive used by all downstream results on coordinate-ray derivatives and radial harmonics.
why it matters
This definition anchors the derivative calculus in the relativity module and is invoked by coordRay_temporal_spatial (invariance under time shifts), partialDeriv_v2_spatialNormSq (explicit functional derivative), and laplacian_radialInv_zero_no_const (vanishing Laplacian of 1/r). In the Recognition Science framework it encodes the three spatial dimensions forced by T8 of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.