IndisputableMonolith.Relativity.Geometry.RiemannSymmetries
This module defines the fully covariant Riemann tensor by lowering its first index with the metric and collects associated symmetry lemmas. Researchers bridging Recognition Science lattice models to continuum gravity would cite it when passing from discrete J-cost to spacetime curvature. The module consists of definitions and supporting lemmas on tensor properties rather than a single overarching proof.
claimThe fully covariant Riemann tensor is given by $R_{ρσμν} = g_{ρα} R^α_{σμν}$.
background
The module resides in the relativity geometry layer of the Recognition Science framework and imports tensor algebra, metric definitions, Christoffel symbols from the curvature module, and derivative operators. Upstream, the curvature module supplies Christoffel symbols derived from the metric while the derivatives module provides the standard basis vectors $e_μ$. The central definition lowers the first index of the Riemann tensor using the metric tensor.
proof idea
This is a definition module, no proofs. It assembles a sequence of declarations establishing the lowered tensor, torsion-free Christoffel symbols, antisymmetry properties, and the first Bianchi identity.
why it matters in Recognition Science
The module supplies the continuum curvature objects required by the DiscreteBridge module, which connects the RS discrete lattice J-cost theory to continuum GR through the chain J-cost lattice to quadratic defect to lattice Laplacian to Ricci scalar to Einstein tensor to the Einstein field equations.
scope and limits
- Does not derive the Riemann tensor from the J-cost functional equation.
- Does not treat torsion or non-metric compatible connections.
- Does not extend to dimensions other than the three spatial dimensions fixed by the framework.
used by (1)
depends on (4)
declarations in this module (28)
-
def
riemann_lowered -
theorem
christoffel_torsion_free -
theorem
riemann_lowered_antisym_last -
theorem
metric_covariant_deriv_zero -
theorem
partialDeriv_christoffel_sym -
theorem
riemann_first_bianchi -
theorem
riemann_lowered_first_bianchi -
def
riemann_lowered_explicit -
theorem
riemann_lowered_explicit_antisym_first -
def
riemann_lowered_eq_explicit_hypothesis -
theorem
riemann_lowered_eq_explicit -
theorem
riemann_lowered_antisym_first -
theorem
riemann_lowered_pair_exchange -
theorem
riemann_pair_exchange_proof -
def
riemann_trace -
theorem
riemann_trace_antisym -
theorem
christoffel_quadratic_trace_vanishes -
def
riemann_trace_vanishes_hypothesis -
theorem
riemann_trace_vanishes -
theorem
ricci_minus_transpose_eq_trace -
theorem
ricci_tensor_symmetric_thm -
theorem
ricci_tensor_symmetric_proof -
def
MixedPartialsSymmetric -
def
MetricSmooth -
theorem
riemann_trace_vanishes_of_smooth -
theorem
riemann_pair_exchange_from_definition -
structure
CurvatureAxiomsHold -
theorem
curvature_axioms_hold