module module high

`IndisputableMonolith.Relativity.Geometry.RiemannSymmetries`

Module defines the fully covariant (0,4) Riemann tensor by lowering the first index of the mixed Riemann tensor with the metric. Researchers linking discrete J-cost lattices to continuum GR would cite it when constructing the curvature side of the Einstein tensor. Content consists of index-lowering definitions plus symmetry lemmas built directly from imported metric and curvature primitives.

claimThe fully covariant Riemann tensor is given by $R_{ρσμν}=g_{ρα}R^α_{σμν}$.

background

Module resides in the Relativity.Geometry layer of the Recognition Science framework. It imports the metric tensor, Christoffel symbols from the Curvature module, and index operations from Tensor (explicitly marked scaffold, outside the certificate chain). Derivatives supplies the basis vectors used in covariant differentiation. The local setting is the continuum limit that converts lattice quadratic defects into Ricci curvature and the Einstein tensor.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Definitions here are imported by DiscreteBridge, which traces the path J-cost lattice → quadratic defect → lattice Laplacian → Ricci scalar → Einstein tensor → EFE. The lowered Riemann tensor supplies the curvature object required to close that discrete-to-continuum bridge inside the Recognition Science forcing chain.

scope and limits

Does not derive the second Bianchi identity.
Does not treat non-metric compatible connections.
Does not incorporate discrete lattice spacing or phi-ladder parameters.
Does not produce the Einstein field equations themselves.

used by (1)

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

IndisputableMonolith.Relativity.Geometry.DiscreteBridge module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Relativity.Calculus.Derivatives module_import
IndisputableMonolith.Relativity.Geometry.Curvature module_import
IndisputableMonolith.Relativity.Geometry.Metric module_import
IndisputableMonolith.Relativity.Geometry.Tensor module_import

declarations in this module (28)

def riemann_lowered L48
theorem christoffel_torsion_free L58
theorem riemann_lowered_antisym_last L65
theorem metric_covariant_deriv_zero L81
theorem partialDeriv_christoffel_sym L87
theorem riemann_first_bianchi L101
theorem riemann_lowered_first_bianchi L129
def riemann_lowered_explicit L155
theorem riemann_lowered_explicit_antisym_first L185
def riemann_lowered_eq_explicit_hypothesis L238
theorem riemann_lowered_eq_explicit L241
theorem riemann_lowered_antisym_first L253
theorem riemann_lowered_pair_exchange L283
theorem riemann_pair_exchange_proof L316
def riemann_trace L331
theorem riemann_trace_antisym L339
theorem christoffel_quadratic_trace_vanishes L362
def riemann_trace_vanishes_hypothesis L418
theorem riemann_trace_vanishes L421
theorem ricci_minus_transpose_eq_trace L433
theorem ricci_tensor_symmetric_thm L464
theorem ricci_tensor_symmetric_proof L476
def MixedPartialsSymmetric L491
def MetricSmooth L495
theorem riemann_trace_vanishes_of_smooth L518
theorem riemann_pair_exchange_from_definition L564
structure CurvatureAxiomsHold L573
theorem curvature_axioms_hold L582