IndisputableMonolith.Relativity.Geometry.RiemannSymmetries
This module defines the fully covariant Riemann tensor by lowering its first index with the metric and assembles related symmetry lemmas. Researchers mapping Recognition Science lattice defects to continuum curvature would cite it inside the discrete-to-continuum bridge. The module imports tensor, metric, curvature, and derivative primitives and adds no new proofs beyond those definitions.
claimThe lowered Riemann tensor is given by $R_{\rho\sigma\mu\nu} = g_{\rho\alpha} R^\alpha{}_{\sigma\mu\nu}$.
background
The module belongs to the relativity geometry layer that converts Recognition Science discrete structures into continuum general relativity. It imports the tensor algebra, the metric tensor, Christoffel symbols (from the curvature module), and partial derivatives. The supplied definition lowers the first index of the mixed Riemann tensor using the metric.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the continuum curvature object required by DiscreteBridge, which traces the path 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 Einstein field equations.
- Does not address the discrete J-cost lattice directly.
- Does not invoke the phi-ladder or Recognition Composition Law.
- Does not compute explicit component expansions.
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