partialDeriv_v2_radialInv
The directional derivative of the radial inverse-power function 1/r^n is computed explicitly in four-dimensional coordinates. Researchers deriving Laplacians or second derivatives for potentials in relativity or electrostatics would cite this when reducing radial calculations to coordinate components. The proof splits into temporal and spatial cases, applying the constant derivative for time and the quotient rule combined with the known derivative of the radius for space.
claimLet $r(x)$ denote the spatial radius of the four-vector $x$. For the function $f(x) = r(x)^{-n}$, the partial derivative satisfies $∂_μ f(x) = 0$ if $μ=0$ and $∂_μ f(x) = -n x_μ r(x)^{-(n+2)}$ otherwise, whenever $r(x) ≠ 0$.
background
In this module spatialRadius denotes the Euclidean norm of the spatial components of a four-vector. The function radialInv n maps a point to the reciprocal of that norm raised to the power n. partialDeriv_v2 supplies the directional derivative along a coordinate axis, extending the placeholder interface defined in the Hamiltonian module. The local setting is the calculus of radial functions on Minkowski space, preparing explicit formulas for potentials that appear in Poisson and wave equations. This result rests on the upstream lemma partialDeriv_v2_spatialRadius_proved, which states that the derivative of the radius itself equals x_μ / r for spatial indices.
proof idea
The proof unfolds the definitions and splits on whether the index μ equals zero. The temporal case reduces the composition along the coordinate ray to a constant via spatialRadius_coordRay_temporal and invokes deriv_const. The spatial case cases on n, establishes HasDerivAt for the radius power and its reciprocal using pow and inv rules, then applies algebraic simplification with ring and power identities to reach the target expression -n x_μ / r^{n+2}.
why it matters in Recognition Science
This supplies the explicit first derivative required by secondDeriv_radialInv and laplacian_radialInv_n_proved. It closes one of the six remaining calculus axioms listed in §XXIII.B′ and directly supports Laplacian computations for inverse-power radial functions that arise in gravitational and electrostatic potentials within the Recognition framework. The result feeds the chain of radial derivative identities used in the broader relativity calculus.
scope and limits
- Does not apply when spatial radius vanishes.
- Does not cover non-integer or negative n.
- Does not address differentiability at the spatial origin.
- Does not extend to non-coordinate directions.
formal statement (Lean)
509theorem partialDeriv_v2_radialInv (n : ℕ) (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
510 partialDeriv_v2 (radialInv n) μ x =
511 if μ = 0 then 0 else - (n : ℝ) * x μ / (spatialRadius x) ^ (n + 2) := by
proof body
Tactic-mode proof.
512 unfold partialDeriv_v2 radialInv
513 by_cases hμ : μ = 0
514 · simp only [hμ, ↓reduceIte]
515 have h : ∀ t, spatialRadius (coordRay x 0 t) = spatialRadius x :=
516 spatialRadius_coordRay_temporal x
517 have h2 : (fun t => 1 / spatialRadius (coordRay x 0 t) ^ n) =
518 (fun _ => 1 / spatialRadius x ^ n) := by
519 funext t; rw [h]
520 simp_rw [h2]; exact deriv_const 0 _
521 · simp only [hμ, ↓reduceIte]
522 cases n with
523 | zero => simp
524 | succ k =>
525 have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
526 have h_r_da : DifferentiableAt ℝ (fun t => spatialRadius (coordRay x μ t)) 0 :=
527 differentiableAt_coordRay_spatialRadius x μ hx
528 have h_r_pow_da : DifferentiableAt ℝ (fun t => spatialRadius (coordRay x μ t) ^ (k + 1)) 0 :=
529 h_r_da.pow (k + 1)
530 have h_r_pow_ne : spatialRadius (coordRay x μ 0) ^ (k + 1) ≠ 0 := by
531 simp only [coordRay_zero]
532 exact pow_ne_zero (k + 1) hx
533 have h_r_deriv : deriv (fun t => spatialRadius (coordRay x μ t)) 0 = x μ / spatialRadius x := by
534 have := partialDeriv_v2_spatialRadius μ x hx
535 simp only [partialDeriv_v2, hμ, ↓reduceIte] at this
536 exact this
537 have h_r_hda : HasDerivAt (fun t => spatialRadius (coordRay x μ t)) (x μ / spatialRadius x) 0 := by
538 have : HasDerivAt (fun t => spatialRadius (coordRay x μ t))
539 (deriv (fun t => spatialRadius (coordRay x μ t)) 0) 0 := h_r_da.hasDerivAt
540 simpa [h_r_deriv] using this
541 have h_rpow_hda : HasDerivAt (fun t => spatialRadius (coordRay x μ t) ^ (k + 1))
542 (↑(k + 1) * spatialRadius x ^ k * (x μ / spatialRadius x)) 0 := by
543 have h1 := h_r_hda.pow (k + 1)
544 simp only [coordRay_zero] at h1
545 convert h1 using 2
546 have h_rinv_hda : HasDerivAt (fun t => (spatialRadius (coordRay x μ t) ^ (k + 1))⁻¹)
547 (-(↑(k + 1) * spatialRadius x ^ k * (x μ / spatialRadius x)) /
548 (spatialRadius x ^ (k + 1)) ^ 2) 0 := by
549 have h2 := h_rpow_hda.inv h_r_pow_ne
550 simp only [coordRay_zero] at h2
551 exact h2
552 have h_inv : (fun t => 1 / spatialRadius (coordRay x μ t) ^ (k + 1)) = fun t => (spatialRadius (coordRay x μ t) ^ (k + 1))⁻¹ := by funext t; exact one_div _
553 rw [h_inv, h_rinv_hda.deriv]
554 have hr_ne : spatialRadius x ≠ 0 := hx
555 have h_pow1 : (spatialRadius x ^ (k + 1)) ^ 2 = spatialRadius x ^ (2 * k + 2) := by
556 rw [← pow_mul]; congr 1; omega
557 have h_pow2 : k + 1 + 2 = k + 3 := by omega
558 rw [div_eq_div_iff]
559 · change -(↑(k + 1) * spatialRadius x ^ k * (x μ / spatialRadius x)) * spatialRadius x ^ (k + 1 + 2) = -↑(k + 1) * x μ * (spatialRadius x ^ (k + 1)) ^ 2
560 rw [h_pow1]
561 rw [h_pow2]
562 calc -(↑(k + 1) * spatialRadius x ^ k * (x μ / spatialRadius x)) * spatialRadius x ^ (k + 3)
563 _ = -(↑(k + 1) * spatialRadius x ^ k * (x μ * (spatialRadius x)⁻¹)) * spatialRadius x ^ (k + 3) := by rw [div_eq_mul_inv]
564 _ = -↑(k + 1) * x μ * (spatialRadius x ^ k * (spatialRadius x)⁻¹ * spatialRadius x ^ (k + 3)) := by ring
565 _ = -↑(k + 1) * x μ * (spatialRadius x ^ k * spatialRadius x ^ (k + 3) * (spatialRadius x)⁻¹) := by ring
566 _ = -↑(k + 1) * x μ * (spatialRadius x ^ (2 * k + 3) * (spatialRadius x)⁻¹) := by
567 have : spatialRadius x ^ k * spatialRadius x ^ (k + 3) = spatialRadius x ^ (2 * k + 3) := by rw [← pow_add]; congr 1; omega
568 rw [this]
569 _ = -↑(k + 1) * x μ * (spatialRadius x ^ (2 * k + 2) * spatialRadius x * (spatialRadius x)⁻¹) := by
570 have : spatialRadius x ^ (2 * k + 2) * spatialRadius x = spatialRadius x ^ (2 * k + 3) := by
571 calc spatialRadius x ^ (2 * k + 2) * spatialRadius x
572 _ = spatialRadius x ^ (2 * k + 2) * spatialRadius x ^ 1 := by rw [pow_one]
573 _ = spatialRadius x ^ (2 * k + 2 + 1) := by rw [← pow_add]
574 _ = spatialRadius x ^ (2 * k + 3) := by rfl
575 rw [← this]
576 _ = -↑(k + 1) * x μ * (spatialRadius x ^ (2 * k + 2) * (spatialRadius x * (spatialRadius x)⁻¹)) := by ring
577 _ = -↑(k + 1) * x μ * (spatialRadius x ^ (2 * k + 2) * 1) := by rw [mul_inv_cancel₀ hr_ne]
578 _ = -↑(k + 1) * x μ * spatialRadius x ^ (2 * k + 2) := by ring
579 · exact pow_ne_zero 2 (pow_ne_zero (k + 1) hr_ne)
580 · exact pow_ne_zero (k + 1 + 2) hr_ne
581
582/-- Differentiability of `s ↦ ∂(1/r^n)/∂x_μ` along a coordinate ray.
583
584 For temporal direction (μ = 0), `partialDeriv_v2 (radialInv n) 0 y = 0` whenever
585 `spatialRadius y ≠ 0`, so the function is locally constant 0 near `s = 0`.
586
587 For spatial direction (μ ≠ 0), `partialDeriv_v2 (radialInv n) μ y =
588 -n · y_μ / r(y)^(n+2)` whenever `spatialRadius y ≠ 0`, so the function is
589 locally a quotient of differentiable functions:
590 - numerator `s ↦ -n · (coordRay x ν s)_μ` is linear in `s`
591 - denominator `s ↦ r(coordRay x ν s)^(n+2)` is the `(n+2)`-power of the
592-- ... 5 more lines elided ...