spatialRadius_coordRay_ne_zero_proved
plain-language theorem explainer
The theorem shows that a coordinate-ray perturbation of a four-vector keeps the spatial radius nonzero whenever the original radius is nonzero and the step satisfies |s| < r/2. Researchers deriving radial derivatives or the Laplacian in relativistic models cite it to justify domain restrictions. The tactic proof expands the squared spatial norm to a quadratic in s, bounds the cross term by the original radius via absolute-value sums and a norm comparison, then applies nlinarith and linarith to obtain strict positivity.
Claim. Let $r(x)$ be the Euclidean norm of the three spatial components of the four-vector $x$. If $r(x) > 0$ and $|s| < r(x)/2$, then $r(x + s e_ν) > 0$, where $e_ν$ is the standard basis vector in coordinate direction $ν$ (vanishing on the time component).
background
The module replaces seven axiom declarations in Derivatives.lean with explicit theorems for radial derivatives. spatialRadius extracts the Euclidean length of the spatial part of a Fin 4 → ℝ vector; coordRay adds a scalar multiple of the corresponding basis vector. The local setting is the C2 discharge, which supplies the non-vanishing and differentiability facts needed for quotient and chain rules on expressions involving 1/spatialRadius and its Laplacian.
proof idea
The proof rewrites the goal via spatialRadius_ne_zero_iff, obtains positivity of the original radius, and expands spatialNormSq(coordRay x ν s) by ring into r² + 2s A + s² B. It bounds |A| ≤ r by summing absolutes, applying abs_mul, and comparing the sum of absolutes to the norm via a sqrt(3) estimate and nlinarith. B is shown nonnegative by sum_nonneg. A quadratic lower bound r² - 2|s|r is derived by nlinarith, then linarith closes positivity under the step-size hypothesis.
why it matters
The result supplies the ne_zero_holds field of c2DischargeCert, which aggregates the proved radial facts and renders the original axioms in Derivatives.lean dead weight. It closes a key non-vanishing hypothesis required for the full C2 discharge in the relativity calculus. In the Recognition framework it supports differentiability steps that feed into mass formulas and phi-ladder constructions by keeping perturbed points inside the domain where spatial norms remain positive and differentiable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.