module module high

`IndisputableMonolith.Relativity.Calculus.Derivatives`

This module supplies the coordinate basis vectors, rays, and partial derivative operators required for tensor calculus on pseudo-Riemannian manifolds. It is imported by the covariant derivative, curvature, and discrete-bridge modules that assemble the Einstein tensor from lattice J-cost. All content consists of direct definitions with no proof obligations.

claimThe module defines the standard basis $e_\mu$, the coordinate ray function, the first partial derivative $\partial_\mu$, the second derivative, the Laplacian, and the linear derivative addition rule on tensor fields.

background

The module lives inside the relativity calculus layer and imports only the tensor geometry definitions. Its sibling declarations introduce the objects that later modules use to write $\nabla_\rho T^\lambda_{\mu\nu} = \partial_\rho T^\lambda_{\mu\nu} + \Gamma^\lambda_{\rho\sigma} T^\sigma_{\mu\nu} - \dots$. The upstream Tensor module is explicitly marked scaffolding and is excluded from the certificate chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The declarations feed the covariant-derivative and curvature modules that construct the Christoffel symbols and the Levi-Civita connection; those in turn supply the Ricci scalar and Einstein tensor inside the discrete-to-continuum bridge that converts lattice J-cost into the Einstein field equations.

scope and limits

Does not prove any derivative identities or chain rules.
Does not define the metric tensor or connection coefficients.
Does not reference the J-cost functional or the phi-ladder.
Does not address discrete lattice structure or Berry creation.

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