c2DischargeCert
plain-language theorem explainer
This definition constructs a concrete instance of the C2 discharge certificate by binding each of its five fields to an explicit theorem that replaces an earlier axiom. Researchers verifying the relativity calculus layer would cite the resulting certificate to confirm that all radial derivative and Laplacian identities hold by proof. The construction is a direct record literal that wires the non-vanishing, partial-derivative, differentiability, and harmonic lemmas into the structure.
Claim. Let $C$ be the structure whose fields assert: (i) spatial radius remains nonzero along any coordinate ray for small displacements when the base point has nonzero radius; (ii) the directional derivative of the spatial radius equals $x_μ/r$ in spatial directions and zero in the time direction; (iii) the directional derivative of $r^{-n}$ equals $-n x_μ/r^{n+2}$ in spatial directions; (iv) the map along a coordinate ray of the partial derivative of $r^{-n}$ is differentiable at the origin; (v) the Laplacian of $1/r$ vanishes wherever the radius is nonzero. The definition $c$ is the element of $C$ obtained by substituting the corresponding proved statements for each field.
background
In this module the spatial radius is the Euclidean norm over the three spatial coordinates of a point in four-dimensional Minkowski space. The radial inverse of order $n$ is the scalar function $1$ over that norm to the power $n$. The operator partialDeriv_v2 extracts the directional derivative in coordinate direction $μ$, while the Laplacian sums the second partials. The module replaces seven axiom declarations that previously appeared in Derivatives.lean. Those axioms are now discharged by explicit proofs that invoke the chain rule for square roots, the quotient rule, and prior results on the spatial norm squared and its differentiability along rays.
proof idea
The definition is a one-line record constructor that directly supplies the five proved lemmas to the fields of the C2DischargeCert structure. It assigns the non-vanishing statement along coordinate rays, the explicit first partial of the spatial radius, the explicit first partial of the radial inverse, the differentiability statement at the ray origin, and the vanishing Laplacian of $1/r$. No additional tactics or reductions are performed.
why it matters
The definition supplies the concrete witness required to inhabit the C2DischargeCert structure, thereby closing the discharge of the original seven axioms. It is referenced by the immediate downstream theorem that proves the structure is nonempty. Within the Recognition Science framework this step converts the radial-Laplacian identities from assumed to derived, supporting the transition to fully proved statements in the relativity calculus layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.