pith. sign in
module module high

IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs

show as:
view Lean formalization →

This module supplies a collection of proved lemmas on the spatial radius along coordinate rays, including non-vanishing conditions, first and second partial derivatives, and Laplacian identities. Researchers formalizing the radial sector of the relativity calculus in Recognition Science would cite these results to discharge differentiability requirements. The proofs consist of direct applications of Mathlib analysis tactics to the imported derivative definitions.

claimIf $r(x) > 0$ and $|s| < r(x)/2$ then $r(x + s e_ν) > 0$, where $r$ denotes spatial radius and $e_ν$ the coordinate ray direction. The module further establishes that the first partial derivative of $r$ along the ray equals the normalized direction, that the second derivative of the radial inverse vanishes, and that the Laplacian of the radial inverse equals zero in the absence of a constant term.

background

The module imports the Derivatives module, whose central object is the standard basis vector $e_μ$ used to define directional derivatives. In the Recognition Science setting, spatialRadius measures the Euclidean length in the three-dimensional spatial slice while coordRay parametrizes motion along a fixed direction $ν$ at signed distance $s$. These objects appear inside the radial sector of the relativity calculus to support later Laplacian and wave-operator constructions.

proof idea

The module is a sequence of standalone proved declarations. Each applies Mathlib's differentiableAt and partialDeriv lemmas to the imported coordRay and spatialRadius definitions, followed by algebraic simplification of the resulting expressions. One-line wrappers discharge the non-vanishing claim and the zero-Laplacian identity; longer tactic blocks handle the second-derivative and C2-discharge certificates.

why it matters in Recognition Science

The lemmas close the radial derivative layer required by the parent Derivatives module and supply the C2DischargeCert needed for higher-order calculus in the relativity section. They thereby support the transition from coordinate definitions to the Laplacian identities used in the eight-tick octave and D=3 spatial structure of the forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)