spatialRadius
plain-language theorem explainer
spatialRadius defines the Euclidean length of the spatial part of a four-vector as the positive square root of the sum of squares of its last three components. Relativists and Recognition Science workers cite it for all radial derivative and Laplacian identities away from the origin. The definition is a direct one-line wrapper of Real.sqrt around spatialNormSq.
Claim. For a four-vector $x : Fin 4 → ℝ$, the spatial radius is $r(x) := √(x_1² + x_2² + x_3²)$.
background
The Derivatives module works with the standard basis vectors e_μ on ℝ⁴. spatialNormSq supplies the squared spatial norm x(1)² + x(2)² + x(3)². spatialRadius then extracts the positive square root, yielding the ordinary radial coordinate r in three spatial dimensions. This matches the upstream definition exactly: “Spatial norm squared x₁² + x₂² + x₃².”
proof idea
One-line wrapper that applies Real.sqrt to spatialNormSq.
why it matters
The definition is invoked by twenty-six downstream theorems, among them differentiableAt_coordRay_spatialRadius, laplacian_radialInv_n and laplacian_radialInv_zero_no_const. The last two close Mathlib calculus axioms by showing ∇²(1/r) = 0 and ∇²(1/r^n) = n(n-1)/r^(n+2) for r ≠ 0. In the Recognition framework it supplies the concrete D = 3 spatial structure required for the phi-ladder mass formula and radial inverses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.