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

IndisputableMonolith.Relativity.Geometry.Tensor

show as:
view Lean formalization →

The Tensor module defines a (p,q) tensor specialized to 4D spacetime together with scalar, vector, covector, and bilinear forms. Researchers building the discrete-to-continuum bridge from lattice J-cost to curvature would import it when constructing covariant derivatives and Ricci scalars. The module supplies only type definitions and basic operations with no theorems or proofs.

claimA $(p,q)$-tensor $T$ on 4-dimensional spacetime, together with scalar fields, vector fields, covector fields, bilinear forms, symmetrization, antisymmetrization, contraction, and tensor product.

background

The module resides in the Relativity.Geometry package and supplies the tensor primitives for the Recognition Science relativity layer. It introduces Tensor as the core (p,q) object in 4D, plus ScalarField, VectorField, CovectorField, BilinearForm, ContravariantBilinear, and the operations symmetrize, antisymmetrize, contract, tensor_product, and zero_tensor. These sit inside the discrete-to-continuum bridge that maps lattice J-cost through quadratic defect and lattice Laplacian to the Ricci scalar and Einstein tensor.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the tensor types required by the Geometry aggregator and by downstream modules CovariantDerivative, Curvature, and DiscreteBridge. It thereby supports the expression of covariant derivatives and Christoffel symbols that close the scaffold from lattice J-cost to the Einstein field equations.

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)