pith. machine review for the scientific record. sign in
theorem proved tactic proof high

partialDeriv_v2_spatialRadius_proved

show as:
view Lean formalization →

The theorem establishes that the directional derivative of the spatial radius equals zero along the time axis and the normalized spatial coordinate otherwise. Researchers computing gradients for radial potentials or Laplacians in recognition-based models cite this identity to replace placeholder derivative axioms. The proof splits on the direction index, using ray invariance for the temporal case and the chain rule through the square root for spatial directions.

claimLet $r(x) = (x_1^2 + x_2^2 + x_3^2)^{1/2}$ denote the spatial radius of the four-vector $x$. For each index $μ ∈ {0,1,2,3}$ with $r(x) ≠ 0$, the directional derivative satisfies $∂_μ r(x) = 0$ when $μ=0$ and $∂_μ r(x) = x_μ / r(x)$ otherwise, where $∂_μ$ is realized by the partialDeriv_v2 operator.

background

spatialRadius is the Euclidean norm of the three spatial components of a four-vector, defined via the square root of spatialNormSq. partialDeriv_v2 is the directional derivative interface for recognition fields, initially introduced as a placeholder in the Hamiltonian module. The module RadialDerivativesProofs replaces seven axioms from Derivatives.lean with explicit theorems, relying on upstream lemmas such as spatialNormSq_coordRay_temporal (invariance of the spatial norm under temporal ray extensions) and partialDeriv_v2_spatialNormSq (derivative of the squared norm equals twice the coordinate).

proof idea

The tactic proof unfolds partialDeriv_v2 and spatialRadius, then cases on whether μ equals zero. The temporal branch invokes spatialNormSq_coordRay_temporal to obtain constancy along the ray and applies deriv_const. The spatial branch confirms positivity via spatialRadius_ne_zero_iff, obtains DifferentiableAt via differentiableAt_coordRay_spatialNormSq, extracts the squared-norm derivative via partialDeriv_v2_spatialNormSq, lifts to HasDerivAt, applies HasDerivAt.sqrt, and simplifies the quotient algebraically with ring_nf and norm_num.

why it matters in Recognition Science

This identity discharges one of the C2 axioms for radial calculus and is referenced directly by c2DischargeCert, partialDeriv_v2_radialInv_proved, and secondDeriv_radialInv_proved. It supplies the concrete derivative needed for inverse-power potentials and Laplacian identities that appear in the recognition framework's three-dimensional spatial sector (T8). The result closes a scaffolding gap between the placeholder partialDeriv_v2 and downstream wave-equation or potential computations.

scope and limits

Lean usage

have h := partialDeriv_v2_spatialRadius_proved μ x hx

formal statement (Lean)

 129theorem partialDeriv_v2_spatialRadius_proved
 130    (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
 131    partialDeriv_v2 spatialRadius μ x =
 132    if μ = 0 then 0 else x μ / spatialRadius x := by

proof body

Tactic-mode proof.

 133  unfold partialDeriv_v2 spatialRadius
 134  by_cases hμ : μ = 0
 135  · -- Temporal direction: spatialNormSq is constant along t ↦ coordRay x 0 t
 136    simp only [hμ, ↓reduceIte]
 137    have h : ∀ t, spatialNormSq (coordRay x 0 t) = spatialNormSq x :=
 138      spatialNormSq_coordRay_temporal x
 139    simp_rw [h]
 140    exact deriv_const 0 _
 141  · -- Spatial direction: apply HasDerivAt.sqrt + chain rule
 142    simp only [hμ, ↓reduceIte]
 143    have h_sn_pos : 0 < spatialNormSq x := by
 144      have := (spatialRadius_ne_zero_iff x).mp hx
 145      exact lt_of_le_of_ne (spatialNormSq_nonneg x) this.symm
 146    -- spatialNormSq along the ray is differentiable with derivative 2 * x μ
 147    have h_sn_da : DifferentiableAt ℝ (fun t => spatialNormSq (coordRay x μ t)) 0 :=
 148      differentiableAt_coordRay_spatialNormSq x μ
 149    have h_sn_deriv : deriv (fun t => spatialNormSq (coordRay x μ t)) 0 = 2 * x μ := by
 150      have := partialDeriv_v2_spatialNormSq μ x
 151      simp only [hμ, ↓reduceIte] at this
 152      exact this
 153    -- HasDerivAt for spatialNormSq ∘ coordRay
 154    have h_sn_hda : HasDerivAt (fun t => spatialNormSq (coordRay x μ t)) (2 * x μ) 0 :=
 155      h_sn_deriv ▸ h_sn_da.hasDerivAt
 156    -- Chain rule for sqrt: HasDerivAt √f
 157    have h_sqrt_hda : HasDerivAt (fun t => Real.sqrt (spatialNormSq (coordRay x μ t)))
 158        ((2 * x μ) / (2 * Real.sqrt (spatialNormSq x))) 0 := by
 159      have h0 : spatialNormSq (coordRay x μ 0) = spatialNormSq x := by
 160        simp [coordRay_zero]
 161      rw [show (2 * x μ) / (2 * Real.sqrt (spatialNormSq x)) =
 162              (2 * x μ) / (2 * Real.sqrt (spatialNormSq (coordRay x μ 0))) by rw [h0]]
 163      exact h_sn_hda.sqrt (by rw [h0]; exact h_sn_pos)
 164    -- Extract the derivative value
 165    rw [h_sqrt_hda.deriv]
 166    -- Simplify: (2 * x μ) / (2 * √(spatialNormSq x)) = x μ / spatialRadius x
 167    unfold spatialRadius
 168    ring_nf
 169    rw [div_div, mul_comm 2 _, ← div_div]
 170    norm_num
 171
 172/-! ## 3. `partialDeriv_v2_radialInv` -/
 173
 174/-- The directional derivative of `1/r^n` in the spatial directions. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (27)

Lean names referenced from this declaration's body.