module module high

`IndisputableMonolith.Relativity.Calculus.Derivatives`

The Derivatives module supplies definitions for standard basis vectors and basic differential operators required for tensor calculus in the Recognition Science relativity setting. It is imported by nine modules that build covariant derivatives, curvature, and the discrete-to-continuum bridge. Content consists solely of definitions with zero proof bodies.

claimDefines the standard basis vector $e_μ$, the coordinate ray, the partial derivative operator $∂_v$, the second derivative, and the Laplacian $∇²$ on the pseudo-Riemannian manifold equipped with the metric tensor.

background

The module sits in the Relativity domain and imports the Tensor module, which is explicitly marked as a scaffold module outside the certificate chain. It introduces basisVec for the standard basis $e_μ$ together with partialDeriv_v2, secondDeriv, and laplacian operators. These objects operate on the coordinate structures supplied by the upstream Tensor definitions and support the J-cost lattice to continuum curvature path described in the DiscreteBridge module.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the derivative primitives used by the Calculus aggregator, RadialDerivativesProofs (which replaces seven axioms with theorems via HasDerivAt and deriv rules), CovariantDerivative (defining $∇ρ T^λ{μν} = ∂ρ T^λ{μν} + Γ$ terms), Curvature, DiscreteBridge (lattice J-cost → quadratic defect → Laplacian → Ricci scalar → Einstein tensor), LeviCivitaTheorem, Metric, and ParallelTransport. It therefore anchors the discrete-to-continuum architecture that connects Recognition Science lattice theory to the Einstein field equations.

scope and limits

Does not contain any proved theorems or proof bodies.
Does not discharge the scaffolding status of the imported Tensor module.
Does not supply the radial derivative theorems later proved in RadialDerivativesProofs.

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