spatialRadius_pos_iff
plain-language theorem explainer
The equivalence between a positive spatial radius and a positive spatial norm squared holds for any four-vector. Relativity calculus workers cite it when confirming that spatial distances vanish only for the zero vector in the spatial sector. The proof is a term-mode reduction that unfolds the square-root definition and applies the library fact on square-root positivity.
Claim. For any $x : Fin 4 → ℝ$, one has $0 < r(x) ↔ 0 < s(x)$, where $r(x) = √(x₁² + x₂² + x₃²)$ and $s(x) = x₁² + x₂² + x₃²$.
background
The derivatives module builds calculus operators on four-vectors, importing tensor geometry for coordinate access. Spatial norm squared is the sum of squares on indices 1, 2, 3. Spatial radius is the non-negative square root of that sum, supplying a length measure for the spatial sector. These definitions precede partial derivatives and Laplacians in the same file.
proof idea
The term proof unfolds the spatialRadius definition, exposing the square root of spatialNormSq. It then rewrites with the Mathlib lemma Real.sqrt_pos, which directly encodes √y > 0 ↔ y > 0.
why it matters
The result is invoked by spatialRadius_pos_of_ne_zero to conclude that a nonzero radius is positive. It supplies a basic positivity check inside the spatial derivatives, supporting later coordinate-ray and second-derivative constructions. The equivalence aligns with the three-dimensional spatial sector required by the framework's eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.