Encyclopedia Relativity Relativity Calculus Derivatives

ARTICLE 6 claims 4 theorems 2 models

Relativity Calculus Derivatives

The module builds the calculus of spacetime, showing how derivatives behave along the four coordinate directions and what they reveal about radial functions.

Verify this page

The derivative toolkit

In the framework of Recognition Science, the ledger (a discrete record of events) is modeled on a four-dimensional spacetime. Each point in this spacetime is described by four coordinates: one temporal and three spatial. The module Relativity.Calculus.Derivatives builds the differential calculus on this spacetime, defining partial derivatives, second derivatives, and the Laplacian, then proving how these operators act on functions that depend only on the spatial distance from the origin.

The core definitions are direct. A basis vector e_μ points along one of the four coordinate axes, and a coordinate ray x + t e_μ moves from a point x in that direction. The partial derivative of a function f along coordinate μ at point x is the ordinary derivative of f along this ray, evaluated at t = 0. The second derivative along two coordinates is defined similarly, by differentiating along one ray and then the other. The Laplacian is the sum of the second derivatives along the three spatial coordinates, omitting time.

The module proves several concrete facts about these operators. The derivative of the squared coordinate x_i^2 along coordinate μ is 2 x_i if i = μ and zero otherwise, matching the familiar single-variable rule. The derivative of the spatial radius r is zero along the time axis and x_μ / r along a spatial axis. For the inverse power 1/r^n, the derivative is zero along time and -n x_μ / r^(n+2) along space.

These results culminate in the Laplacian of 1/r^n. The theorem states that laplacian (radialInv n) x = n (n - 1) / r^(n + 2) when the spatial radius is nonzero. In particular, for n = 1, the Laplacian of 1/r is zero away from the origin. This is the classical harmonic function result, proved here within the framework's own coordinate system. The module also establishes differentiability conditions, ensuring these derivatives are well-defined wherever the spatial radius does not vanish.

In Recognition Science, this calculus is the groundwork for field equations. The fact that 1/r is harmonic in three spatial dimensions is the seed of inverse-square laws, and the framework's library proves this property from its own definitions rather than importing it. The module does not yet connect these derivatives to physical forces or particle behavior; it supplies the differential machinery those connections will use.

MODEL partialDeriv_v2 · IndisputableMonolith/Relativity/Calculus/Derivatives.lean
partialDeriv_v2 · IndisputableMonolith/Relativity/Calculus/Derivatives.lean:33 
/-- Directional derivative `∂_μ f(x)` via real derivative along the coordinate ray. -/
noncomputable def partialDeriv_v2 (f : (Fin 4 → ℝ) → ℝ) (μ : Fin 4)
    (x : Fin 4 → ℝ) : ℝ :=
  deriv (fun t => f (coordRay x μ t)) 0
MODEL laplacian · IndisputableMonolith/Relativity/Calculus/Derivatives.lean
laplacian · IndisputableMonolith/Relativity/Calculus/Derivatives.lean:53 
/-- Laplacian `∇² = Σ_{i=1}^3 ∂²/∂xᵢ²`. -/
noncomputable def laplacian (f : (Fin 4 → ℝ) → ℝ) (x : Fin 4 → ℝ) : ℝ :=
  secondDeriv f ⟨1, by decide⟩ ⟨1, by decide⟩ x +
  secondDeriv f ⟨2, by decide⟩ ⟨2, by decide⟩ x +
  secondDeriv f ⟨3, by decide⟩ ⟨3, by decide⟩ x
THEOREM partialDeriv_v2_x_sq · IndisputableMonolith/Relativity/Calculus/Derivatives.lean
partialDeriv_v2_x_sq · IndisputableMonolith/Relativity/Calculus/Derivatives.lean:364 
/-- Closed form for ∂μ (xᵢ²). -/
theorem partialDeriv_v2_x_sq (μ i : Fin 4) (x : Fin 4 → ℝ) :
    partialDeriv_v2 (fun y => y i ^ 2) μ x = 2 * x i * (if i = μ then 1 else 0) := by
  unfold partialDeriv_v2
  simp only [coordRay_apply]
  let f_i := fun t => x i + t * basisVec μ i
  have h_f : DifferentiableAt ℝ f_i 0 := differentiableAt_coordRay_i x μ i
  rw [show (fun t => (x i + t * basisVec μ i) ^ 2) = f_i ^ 2 by rfl]
  rw [deriv_pow h_f 2]
  simp only [f_i]
  split_ifs with h_eq
  · subst h_eq
    simp only [basisVec_self, mul_one]
    rw [deriv_const_add, deriv_id'']
    ring
  · simp only [basisVec_ne h_eq, mul_zero, add_zero]
    rw [deriv_const]
    ring
THEOREM partialDeriv_v2_radialInv · IndisputableMonolith/Relativity/Calculus/Derivatives.lean
partialDeriv_v2_radialInv · IndisputableMonolith/Relativity/Calculus/Derivatives.lean:501 
/-- Directional derivative of `radialInv` in coordinates.

    For temporal direction (μ = 0), `radialInv` is invariant along the ray,
    so the derivative is 0. For a spatial direction (μ ≠ 0), we use the quotient
    rule `HasDerivAt.div` on `1 / r^n`, composing with `HasDerivAt.pow` and
    the derivative `∂_μ r = x_μ / r` (lifted from `partialDeriv_v2_spatialRadius`).

    Closes one of the six remaining §XXIII.B′ Mathlib calculus axioms. -/
theorem partialDeriv_v2_radialInv (n : ℕ) (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
    partialDeriv_v2 (radialInv n) μ x =
    if μ = 0 then 0 else - (n : ℝ) * x μ / (spatialRadius x) ^ (n + 2) := by
  unfold partialDeriv_v2 radialInv
  by_cases hμ : μ = 0
  · simp only [hμ, ↓reduceIte]
    have h : ∀ t, spatialRadius (coordRay x 0 t) = spatialRadius x :=
      spatialRadius_coordRay_temporal x
    have h2 : (fun t => 1 / spatialRadius (coordRay x 0 t) ^ n) =
              (fun _ => 1 / spatialRadius x ^ n) := by
      funext t; rw [h]
    simp_rw [h2]; exact deriv_const 0 _
  · simp only [hμ, ↓reduceIte]
    cases n with
    | zero => simp
    | succ k =>
      have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
      have h_r_da : DifferentiableAt ℝ (fun t => spatialRadius (coordRay x μ t)) 0 :=
        differentiableAt_coordRay_spatialRadius x μ hx
      have h_r_pow_da : DifferentiableAt ℝ (fun t => spatialRadius (coordRay x μ t) ^ (k + 1)) 0 :=
        h_r_da.pow (k + 1)
      have h_r_pow_ne : spatialRadius (coordRay x μ 0) ^ (k + 1) ≠ 0 := by
        simp only [coordRay_zero]
        exact pow_ne_zero (k + 1) hx
      have h_r_deriv : deriv (fun t => spatialRadius (coordRay x μ t)) 0 = x μ / spatialRadius x := by
        have := partialDeriv_v2_spatialRadius μ x hx
        simp only [partialDeriv_v2, hμ, ↓reduceIte] at this
        exact this
      have h_r_hda : HasDerivAt (fun t => spatialRadius (coordRay x μ t)) (x μ / spatialRadius x) 0 := by
        have : HasDerivAt (fun t => spatialRadius (coordRay x μ t))
            (deriv (fun t => spatialRadius (coordRay x μ t)) 0) 0 := h_r_da.hasDerivAt
        simpa [h_r_deriv] using this
      have h_rpow_hda : HasDerivAt (fun t => spatialRadius (coordRay x μ t) ^ (k + 1))
          (↑(k + 1) * spatialRadius x ^ k * (x μ / spatialRadius x)) 0 := by
        have h1 := h_r_hda.pow (k + 1)
        simp only [coordRay_zero] at h1
        convert h1 using 2
      have h_rinv_hda : HasDerivAt (fun t => (spatialRadius (coordRay x μ t) ^ (k + 1))⁻¹)
          (-(↑(k + 1) * spatialRadius x ^ k * (x μ / spatialRadius x)) /
             (spatialRadius x ^ (k + 1)) ^ 2) 0 := by
        have h2 := h_rpow_hda.inv h_r_pow_ne
        simp only [coordRay_zero] at h2
        exact h2
      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 _
      rw [h_inv, h_rinv_hda.deriv]
      have hr_ne : spatialRadius x ≠ 0 := hx
      have h_pow1 : (spatialRadius x ^ (k + 1)) ^ 2 = spatialRadius x ^ (2 * k + 2) := by
        rw [← pow_mul]; congr 1; omega
      have h_pow2 : k + 1 + 2 = k + 3 := by omega
      rw [div_eq_div_iff]
      · change -(↑(k + 1) * spatialRadius x ^ k * (x μ / spatialRadius x)) * spatialRadius x ^ (k + 1 + 2) = -↑(k + 1) * x μ * (spatialRadius x ^ (k + 1)) ^ 2
        rw [h_pow1]
        rw [h_pow2]
        calc -(↑(k + 1) * spatialRadius x ^ k * (x μ / spatialRadius x)) * spatialRadius x ^ (k + 3)
          _ = -(↑(k + 1) * spatialRadius x ^ k * (x μ * (spatialRadius x)⁻¹)) * spatialRadius x ^ (k + 3) := by rw [div_eq_mul_inv]
          _ = -↑(k + 1) * x μ * (spatialRadius x ^ k * (spatialRadius x)⁻¹ * spatialRadius x ^ (k + 3)) := by ring
          _ = -↑(k + 1) * x μ * (spatialRadius x ^ k * spatialRadius x ^ (k + 3) * (spatialRadius x)⁻¹) := by ring
          _ = -↑(k + 1) * x μ * (spatialRadius x ^ (2 * k + 3) * (spatialRadius x)⁻¹) := by
            have : spatialRadius x ^ k * spatialRadius x ^ (k + 3) = spatialRadius x ^ (2 * k + 3) := by rw [← pow_add]; congr 1; omega
            rw [this]
          _ = -↑(k + 1) * x μ * (spatialRadius x ^ (2 * k + 2) * spatialRadius x * (spatialRadius x)⁻¹) := by
            have : spatialRadius x ^ (2 * k + 2) * spatialRadius x = spatialRadius x ^ (2 * k + 3) := by
              calc spatialRadius x ^ (2 * k + 2) * spatialRadius x
                _ = spatialRadius x ^ (2 * k + 2) * spatialRadius x ^ 1 := by rw [pow_one]
                _ = spatialRadius x ^ (2 * k + 2 + 1) := by rw [← pow_add]
                _ = spatialRadius x ^ (2 * k + 3) := by rfl
            rw [← this]
          _ = -↑(k + 1) * x μ * (spatialRadius x ^ (2 * k + 2) * (spatialRadius x * (spatialRadius x)⁻¹)) := by ring
          _ = -↑(k + 1) * x μ * (spatialRadius x ^ (2 * k + 2) * 1) := by rw [mul_inv_cancel₀ hr_ne]
          _ = -↑(k + 1) * x μ * spatialRadius x ^ (2 * k + 2) := by ring
      · exact pow_ne_zero 2 (pow_ne_zero (k + 1) hr_ne)
      · exact pow_ne_zero (k + 1 + 2) hr_ne
THEOREM laplacian_radialInv_n · IndisputableMonolith/Relativity/Calculus/Derivatives.lean
laplacian_radialInv_n · IndisputableMonolith/Relativity/Calculus/Derivatives.lean:800 
/-- Laplacian of `1/r^n` for general `n`:
    `∇²(1/r^n) = n(n-1)/r^(n+2)` (away from the origin).

    Sum of diagonal `secondDeriv_radialInv n i i x` over `i ∈ {1,2,3}`:
    `n · ((n+2) ‖x‖² / r^(n+4) - 3/r^(n+2)) = n · ((n+2)/r^(n+2) - 3/r^(n+2))`
    `= n(n-1)/r^(n+2)` (using `‖x‖² = r²`).

    Closes one of the §XXIII.B′ Mathlib calculus axioms. -/
theorem laplacian_radialInv_n
    (n : ℕ) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
    laplacian (radialInv n) x =
    (n : ℝ) * ((n : ℝ) - 1) / (spatialRadius x) ^ (n + 2) := by
  unfold laplacian
  have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
  have h1 := secondDeriv_radialInv n (1 : Fin 4) (1 : Fin 4) x hx
  have h2 := secondDeriv_radialInv n (2 : Fin 4) (2 : Fin 4) x hx
  have h3 := secondDeriv_radialInv n (3 : Fin 4) (3 : Fin 4) x hx
  simp only [show ((1 : Fin 4) ≠ 0) from by decide,
             show ((2 : Fin 4) ≠ 0) from by decide,
             show ((3 : Fin 4) ≠ 0) from by decide,
             or_self, ↓reduceIte] at h1 h2 h3
  show secondDeriv (radialInv n) (1 : Fin 4) (1 : Fin 4) x +
       secondDeriv (radialInv n) (2 : Fin 4) (2 : Fin 4) x +
       secondDeriv (radialInv n) (3 : Fin 4) (3 : Fin 4) x =
       (n : ℝ) * ((n : ℝ) - 1) / spatialRadius x ^ (n + 2)
  rw [h1, h2, h3]
  -- Algebraic finish via linear_combination using `r² = x₁² + x₂² + x₃²`.
  have hr_sq : spatialRadius x ^ 2 = x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2 := by
    unfold spatialRadius
    rw [Real.sq_sqrt (spatialNormSq_nonneg x)]; rfl
  have h_pow_n_plus_4 : spatialRadius x ^ (n + 4) =
                        spatialRadius x ^ (n + 2) * spatialRadius x ^ 2 := by
    rw [← pow_add]
  have h_r_n2_ne : spatialRadius x ^ (n + 2) ≠ 0 := pow_ne_zero _ hx
  have h_r_n4_ne : spatialRadius x ^ (n + 4) ≠ 0 := pow_ne_zero _ hx
  field_simp
  rw [h_pow_n_plus_4]
  linear_combination
    (-(n : ℝ) * ((n : ℝ) + 2) * spatialRadius x ^ (n + 2)) * hr_sq
THEOREM laplacian_radialInv_zero_no_const · IndisputableMonolith/Relativity/Calculus/Derivatives.lean
laplacian_radialInv_zero_no_const · IndisputableMonolith/Relativity/Calculus/Derivatives.lean:762 
/-- Laplacian of `1/r` vanishes (the radial inverse is harmonic away from the origin).

    `∇²(1/r) = ∂₁²(1/r) + ∂₂²(1/r) + ∂₃²(1/r)`.
    Each diagonal second-derivative is `3 x_i² / r^5 - 1/r^3` from `secondDeriv_radialInv` at `n = 1`.
    The sum is `3 ‖x‖² / r^5 - 3/r^3 = 3 r² / r^5 - 3/r^3 = 3/r^3 - 3/r^3 = 0`.

    Closes one of the §XXIII.B′ Mathlib calculus axioms. -/
theorem laplacian_radialInv_zero_no_const
    (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
    laplacian (radialInv 1) x = 0 := by
  unfold laplacian
  have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
  -- Use `(1 : Fin 4)`, `(2 : Fin 4)`, `(3 : Fin 4)` to match `spatialNormSq` syntactically.
  have h1 := secondDeriv_radialInv 1 (1 : Fin 4) (1 : Fin 4) x hx
  have h2 := secondDeriv_radialInv 1 (2 : Fin 4) (2 : Fin 4) x hx
  have h3 := secondDeriv_radialInv 1 (3 : Fin 4) (3 : Fin 4) x hx
  simp only [show ((1 : Fin 4) ≠ 0) from by decide,
             show ((2 : Fin 4) ≠ 0) from by decide,
             show ((3 : Fin 4) ≠ 0) from by decide,
             or_self, ↓reduceIte] at h1 h2 h3
  -- The `laplacian` definition uses `⟨i, _⟩ : Fin 4` form, but these are defeq to `(i : Fin 4)`.
  -- Convert via `show` to align indices.
  show secondDeriv (radialInv 1) (1 : Fin 4) (1 : Fin 4) x +
       secondDeriv (radialInv 1) (2 : Fin 4) (2 : Fin 4) x +
       secondDeriv (radialInv 1) (3 : Fin 4) (3 : Fin 4) x = 0
  rw [h1, h2, h3]
  -- Algebraic finish: 3 (x₁² + x₂² + x₃²)/r^5 - 3/r^3 = 0 since x₁² + x₂² + x₃² = r².
  have hr_sq : spatialRadius x ^ 2 = x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2 := by
    unfold spatialRadius
    rw [Real.sq_sqrt (spatialNormSq_nonneg x)]; rfl
  have h_pow5 : spatialRadius x ^ 5 = spatialRadius x ^ 3 * spatialRadius x ^ 2 := by
    rw [← pow_add]
  have h_r3_ne : spatialRadius x ^ 3 ≠ 0 := pow_ne_zero 3 hx
  have h_r5_ne : spatialRadius x ^ 5 ≠ 0 := pow_ne_zero 5 hx
  field_simp
  rw [h_pow5, hr_sq]
  ring

What this page does not claim

The module does not derive any physical force law or field equation. The module does not address the behavior of derivatives at the origin where the spatial radius vanishes. The module does not establish the connection between these derivatives and the framework's recognition cost function.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Relativity/Calculus/Derivatives.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND