spatialRadius_coordRay_ne_zero_eventually
plain-language theorem explainer
The theorem asserts that if the spatial radius of a four-vector x is nonzero, then along any coordinate ray through x the radius stays nonzero in some punctured neighborhood of the origin. Workers on radial derivatives in special relativity cite it to guarantee that 1/r expressions remain smooth near the evaluation point. The argument reduces to continuity of the radius function along the ray together with the elementary fact that a continuous function nonzero at a point is eventually nonzero.
Claim. Let $r(x) = (x_1^2 + x_2^2 + x_3^2)^{1/2}$ denote the spatial radius of $x : Fin 4 → ℝ$. For any $x$ with $r(x) ≠ 0$ and any index $μ$, the map $t ↦ r(x + t e_μ)$ satisfies $r(x + t e_μ) ≠ 0$ for all $t$ sufficiently close to 0, where $e_μ$ is the standard basis vector.
background
In the Relativity.Calculus.Derivatives module the spatial radius is obtained from the spatial norm squared via the square root; the coordinate ray is the affine line $coordRay x μ t = x + t · basisVec μ$. The module opens with the definition of the standard basis vector $e_μ$. This non-vanishing statement supplies the local hypothesis required for chain-rule applications to radial inverses and their derivatives along coordinate directions. Upstream results on ledger factorization and phi-forcing supply the Recognition Science setting in which these coordinate calculations sit, while the immediate technical dependence is on Mathlib continuity and filter lemmas.
proof idea
The proof first records continuity of $t ↦ spatialRadius (coordRay x μ t)$ by unfolding spatialRadius, spatialNormSq, coordRay and basisVec and invoking fun_prop. It then applies the Mathlib fact that a continuous function whose value at zero is nonzero is eventually nonzero, using the supplied hypothesis hx together with the evaluation coordRay x μ 0 = x.
why it matters
The result is invoked directly by differentiableAt_coordRay_partialDeriv_v2_radialInv and by secondDeriv_radialInv, which in turn feed the proved radial-derivative statements in RadialDerivativesProofs. It therefore closes one of the seven calculus axioms listed in §XXIII.B′. In the Recognition framework it guarantees that radial potentials and the phi-ladder remain differentiable away from the spatial origin, supporting the derivation of the eight-tick octave and D = 3 from the J-uniqueness condition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.