module module moderate

`IndisputableMonolith.Relativity.Calculus.Derivatives`

The Derivatives module supplies coordinate calculus primitives including the standard basis vector e_μ and partial derivative operators for tensor fields in pseudo-Riemannian settings. It is cited by modules that build covariant derivatives, curvature, and the lattice-to-continuum bridge. The module consists of definitions for basisVec, partialDeriv_v2, secondDeriv, and laplacian together with elementary algebraic properties.

claimStandard basis vector $e_μ$ and partial derivative operator $∂_v$ on tensor components, with second derivative and Laplacian also defined in coordinate charts.

background

This module sits inside the Relativity.Calculus namespace and builds directly on the tensor structures imported from the Geometry.Tensor module. It introduces the standard basis vector $e_μ$ (with self and distinct-index properties) and the coordinate partial derivative operator partialDeriv_v2 that extracts components along coordRay directions. The upstream Tensor module is explicitly marked as a scaffold and supplies the underlying tensor type but is not part of the certificate chain. Downstream modules such as CovariantDerivative then combine these partials with Christoffel symbols to form the full covariant derivative.

proof idea

This is a definition module. It declares the basis vectors and derivative operators along with basic properties (additivity, constancy under coordRay_zero, and linearity via deriv_add_lin) whose proofs are either immediate or delegated to Mathlib lemmas.

why it matters in Recognition Science

The module provides the differentiation layer required by CovariantDerivative (which defines $∇ρ T^λ{μν} = ∂ρ T^λ{μν} + Γ^λ_{ρσ} T^σ_{μν} - …$), Curvature, and the DiscreteBridge that maps lattice J-cost to Ricci scalar and Einstein equations. It also supplies the operators whose axioms are discharged in RadialDerivativesProofs using HasDerivAt.sqrt and deriv_div. The module therefore closes the coordinate-calculus interface between the core Recognition Science lattice and the continuum GR layer.

scope and limits

Does not define or prove covariant derivatives or Christoffel symbols.
Does not treat non-coordinate bases or general manifold charts.
Does not establish differentiability criteria for arbitrary tensor fields.
Does not connect to J-cost, phi-ladder, or discrete forcing chain steps.

used by (9)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Relativity.Calculus module_import
IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs module_import
IndisputableMonolith.Relativity.Geometry.CovariantDerivative module_import
IndisputableMonolith.Relativity.Geometry.Curvature module_import
IndisputableMonolith.Relativity.Geometry.DiscreteBridge module_import
IndisputableMonolith.Relativity.Geometry.LeviCivitaTheorem module_import
IndisputableMonolith.Relativity.Geometry.Metric module_import
IndisputableMonolith.Relativity.Geometry.ParallelTransport module_import
IndisputableMonolith.Relativity.Geometry.RiemannSymmetries module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Relativity.Geometry.Tensor module_import

declarations in this module (51)

def basisVec L12
lemma basisVec_self L14
lemma basisVec_ne L16
def coordRay L20
lemma coordRay_apply L23
lemma coordRay_zero L26
lemma coordRay_coordRay L29
def partialDeriv_v2 L34
lemma partialDeriv_v2_const L39
def secondDeriv L49
def laplacian L54
lemma deriv_add_lin L60
lemma partialDeriv_v2_smul L69
lemma secondDeriv_smul_local L77
lemma secondDeriv_smul L92
lemma laplacian_smul L105
lemma partialDeriv_v2_mul L114
def spatialNormSq L129
theorem spatialNormSq_nonneg L131
theorem spatialNormSq_eq_zero_iff L135
def spatialRadius L151
theorem spatialRadius_pos_iff L153
theorem spatialRadius_ne_zero_iff L157
theorem spatialRadius_pos_of_ne_zero L162
lemma coordRay_temporal_spatial L168
lemma spatialNormSq_coordRay_temporal L173
lemma spatialRadius_coordRay_temporal L182
lemma sq_le_spatialNormSq_1 L188
lemma sq_le_spatialNormSq_2 L192
lemma sq_le_spatialNormSq_3 L196
lemma spatialNormSq_coordRay_spatial_1 L202
lemma spatialNormSq_coordRay_spatial_2 L210
lemma spatialNormSq_coordRay_spatial_3 L218
theorem spatialRadius_coordRay_ne_zero L239
def radialInv L346
theorem differentiableAt_coordRay_i L350
theorem differentiableAt_coordRay_i_sq L360
theorem partialDeriv_v2_x_sq L365
theorem deriv_coordRay_i L383
theorem deriv_coordRay_j L388
theorem partialDeriv_v2_spatialNormSq L398
theorem differentiableAt_coordRay_spatialNormSq L409
theorem differentiableAt_coordRay_spatialRadius L419
theorem differentiableAt_coordRay_radialInv L428
theorem spatialRadius_coordRay_ne_zero_eventually L442
theorem partialDeriv_v2_spatialRadius L459
theorem partialDeriv_v2_radialInv L509
theorem differentiableAt_coordRay_partialDeriv_v2_radialInv L596
theorem secondDeriv_radialInv L646
theorem laplacian_radialInv_zero_no_const L769
theorem laplacian_radialInv_n L808