C2DischargeCert
The C2DischargeCert structure packages five proved identities for the spatial radius and its radial inverses that replace prior axioms in the relativity calculus layer. Researchers formalizing 4D potentials or Laplacian identities would cite it to confirm the calculus base is now theorem-driven. It is realized as a record type whose fields are directly assigned the corresponding lemmas from the same module.
claimA structure certifying: for $x$ with spatial radius $r(x) > 0$ and short parameter $s$, the perturbed point along any coordinate direction keeps $r > 0$; the directional derivative of $r$ equals the normalized spatial component (zero in time); the directional derivative of $1/r^n$ follows the quotient rule; the map along the ray for that derivative is differentiable at the origin; and the three-dimensional Laplacian of $1/r$ vanishes wherever $r > 0$.
background
The module supplies proved radial calculus identities for use in gravitational potentials. Spatial radius is the Euclidean norm on the last three coordinates. Coordinate ray adds a scalar multiple of a basis vector to a point. Partial derivative is the ordinary derivative of the function composed with the ray, evaluated at zero. Radial inverse supplies $1/r^n$ for integer $n$. Laplacian sums the three spatial second derivatives.
proof idea
This is a definition of a record type. Its fields are populated directly by the five proved theorems in the module: the non-vanishing result along rays, the explicit partial formula for the radius, the quotient-rule formula for the radial inverse, the differentiability statement along rays, and the vanishing Laplacian for $1/r$.
why it matters in Recognition Science
It supplies the single certificate that discharges the radial derivative axioms previously declared in Derivatives.lean, as stated in the module documentation. The structure is instantiated to build c2DischargeCert and to prove the inhabited theorem for the certificate type. This reduces the axiom count in the relativity calculus layer and supports the framework goal of replacing axiomatic calculus with derived results.
scope and limits
- Does not replace the original axiom declarations inside Derivatives.lean.
- Does not establish the identities when spatial radius is zero.
- Does not include time derivatives inside the Laplacian.
- Does not give the Laplacian formula for $1/r^n$ when $n > 1$.
- Does not address differentiability at spatial infinity or global properties.
Lean usage
def c2DischargeCert : C2DischargeCert where ne_zero_holds := spatialRadius_coordRay_ne_zero_proved partial_sr_holds := partialDeriv_v2_spatialRadius_proved partial_inv_holds := partialDeriv_v2_radialInv_proved diff_at_holds := differentiableAt_coordRay_partialDeriv_v2_radialInv_proved lap_zero_holds := laplacian_radialInv_zero_no_const_provedformal statement (Lean)
468structure C2DischargeCert where
469 ne_zero_holds : ∀ (x : Fin 4 → ℝ) (ν : Fin 4) (s : ℝ)
470 (hx : spatialRadius x ≠ 0) (hs : |s| < spatialRadius x / 2),
471 spatialRadius (coordRay x ν s) ≠ 0
472 partial_sr_holds : ∀ (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0),
473 partialDeriv_v2 spatialRadius μ x = if μ = 0 then 0 else x μ / spatialRadius x
474 partial_inv_holds : ∀ (n : ℕ) (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0),
475 partialDeriv_v2 (radialInv n) μ x =
476 if μ = 0 then 0 else -(n : ℝ) * x μ / (spatialRadius x) ^ (n + 2)
477 diff_at_holds : ∀ (n : ℕ) (x : Fin 4 → ℝ) (μ ν : Fin 4) (hx : spatialRadius x ≠ 0),
478 DifferentiableAt ℝ (fun s => partialDeriv_v2 (radialInv n) μ (coordRay x ν s)) 0
479 lap_zero_holds : ∀ (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0),
480 laplacian (radialInv 1) x = 0
481