pith. machine review for the scientific record. sign in
def definition def or abbrev high

spatialNormSq

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 129def spatialNormSq (x : Fin 4 → ℝ) : ℝ := x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2

proof body

Definition body.

 130

used by (26)

From the project-wide theorem graph. These declarations reference this one in their body.