c2DischargeCert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish any identities at the spatial origin where the radius vanishes.
- Does not treat derivatives with respect to the temporal coordinate beyond the zero case.
- Does not extend the formulas to curved metrics or non-flat backgrounds.
- Does not derive higher-order derivatives or the full set of field equations.
Lean usage
theorem c2DischargeCert_inhabited : Nonempty C2DischargeCert := ⟨c2DischargeCert⟩formal statement (Lean)
482def c2DischargeCert : C2DischargeCert where
483 ne_zero_holds := spatialRadius_coordRay_ne_zero_proved
proof body
Definition body.
484 partial_sr_holds := partialDeriv_v2_spatialRadius_proved
485 partial_inv_holds := partialDeriv_v2_radialInv_proved
486 diff_at_holds := differentiableAt_coordRay_partialDeriv_v2_radialInv_proved
487 lap_zero_holds := laplacian_radialInv_zero_no_const_proved
488