pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Relativity.Geometry.Tensor

show as:
view Lean formalization →

The Tensor module defines the basic (p,q)-tensor types specialized to 4D spacetime as a scaffold in the Recognition Science relativity layer. It supplies the algebraic primitives for scalar, vector, covector, and bilinear fields used by all downstream geometry and calculus modules. Researchers extending the discrete J-cost lattice to continuum curvature would cite it as the entry point. The module consists entirely of type and operation definitions with no proofs.

claimA $(p,q)$-tensor on 4-dimensional spacetime, together with the types ScalarField, VectorField, CovectorField, BilinearForm, ContravariantBilinear, the predicates IsSymmetric, and the operations symmetrize, antisymmetrize, contract, tensor_product, and zero_tensor.

background

Recognition Science models spacetime as 4-dimensional (D=3 spatial plus time) and requires tensor algebra to express curvature and derivatives. This module imports Mathlib tensor machinery and specializes it to the (p,q) case for 4D. It introduces the sibling definitions Tensor, ScalarField, VectorField, CovectorField, BilinearForm, ContravariantBilinear, IsSymmetric, symmetrize, antisymmetrize, contract, tensor_product, and zero_tensor. These supply the notation for fields and operations that appear in covariant derivatives and curvature expressions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the Geometry aggregator and the modules Derivatives, Connection, CovariantDerivative, Curvature, DiscreteBridge, LeviCivitaTheorem, and Metric. It supplies the tensor primitives required to state the covariant derivative formula, Christoffel symbols, and the discrete-to-continuum bridge from J-cost lattice to Ricci scalar and Einstein tensor. As the scaffold noted in its doc-comment, it prepares the ground for the full relativity certificate chain.

scope and limits

used by (11)

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

declarations in this module (12)