differentiableAt_coordRay_partialDeriv_v2_radialInv
plain-language theorem explainer
The declaration shows that the map sending s to the partial derivative of 1/r^n with respect to the μ coordinate, evaluated at the point reached by traveling distance s along the ν-ray from x, is differentiable at s=0 whenever the spatial radius at x is nonzero. Analysts verifying smoothness of radial potentials in four-dimensional Minkowski space cite this when closing calculus axioms for derived fields. The tactic proof splits on whether μ is the temporal index, handling the zero case by eventual constancy and the spatial case by quotient of
Claim. Let r denote the spatial radius. For natural number n, point x in R^4 with r(x) ≠ 0, and indices μ, ν in {0,1,2,3}, the map s ↦ ∂_μ (1/r^n) evaluated at the point x + s e_ν is differentiable at s = 0.
background
In this module the partial derivative operator partialDeriv_v2 acts on a scalar field such as radialInv n, which is the function y ↦ 1/r(y)^n. The ray map coordRay x ν s parametrizes the straight line through x in the direction of the standard basis vector e_ν, so that coordRay x ν 0 = x and the spatial radius along the ray remains positive near s = 0 by the hypothesis spatialRadius x ≠ 0. The upstream placeholder partialDeriv_v2 in Foundation.Hamiltonian supplies the interface whose concrete values are later supplied by the radial formula -n y_μ / r^{n+2} for spatial μ. The module itself opens by fixing the standard basis vectors e_μ used to define these coordinate rays.
proof idea
The tactic proof performs case analysis on whether μ equals 0. When μ = 0 the inner partial derivative is identically zero wherever the radius is nonzero, so the composite map is eventually the constant zero function and hence differentiable at zero by the constant-function rule together with an eventually-equal congruence. When μ ≠ 0 the proof first establishes differentiability of the numerator linear in s and of the denominator power of the radius, verifies the denominator is nonzero at s = 0, obtains differentiability of their quotient, and finally applies an eventually-equal congruence that invokes the already-proved radial formula partialDeriv_v2_radialInv.
why it matters
This result supplies the differentiability step required by the downstream theorems laplacian_radialInv_n_proved and partialDeriv_v2_radialInv_proved in RadialDerivativesProofs, which in turn close the explicit Laplacian and first-derivative formulas for 1/r^n. The doc-comment records that it discharges one of the §XXIII.B′ Mathlib calculus axioms needed for the Recognition Science treatment of radial potentials. Within the broader framework the construction supports the eight-tick octave and three-dimensional spatial structure by guaranteeing that derived fields remain differentiable along admissible paths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.