C2DischargeCert
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.