pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry

show as:
view Lean formalization →

The Relativity.Geometry module assembles manifold, metric, connection, curvature, and discrete-bridge primitives to embed Recognition Science lattice defects into pseudo-Riemannian spacetime. Researchers deriving FRW solutions, null geodesics, or gravitational-wave actions would import it. The module itself is a definition hub containing no proofs and simply re-exports nine submodules, most of which remain scaffolds.

claimThe module equips a pseudo-Riemannian manifold $(M,g)$ with a metric $g$, Levi-Civita connection whose Christoffel symbols are derived from $g$, curvature tensors, and a discrete bridge sending lattice J-cost defects through quadratic defects and the lattice Laplacian to the Ricci scalar and Einstein tensor.

background

This module occupies the Relativity domain and imports nine submodules. Manifold supplies a minimal typed manifold placeholder. Connection provides Christoffel symbols that default to zero. Curvature derives those symbols from the metric. LeviCivitaTheorem states that on any pseudo-Riemannian manifold there exists a unique torsion-free, metric-compatible connection. DiscreteBridge states: “This module connects the RS discrete lattice theory to the IM continuum GR: J-cost lattice → quadratic defect → lattice Laplacian → ∇² → Ricci scalar → Einstein tensor → EFE.” ParallelTransport and MetricUnification complete the set.

proof idea

This is a definition module, no proofs. It aggregates the nine imported submodules that together supply the geometric primitives; each submodule is either a scaffold or a short derivation of Christoffel symbols and curvature from the metric.

why it matters in Recognition Science

The module supplies the geometric substrate for nine downstream modules, including Cosmology.FRWMetric, Geodesics.NullGeodesic, GW.ActionExpansion, and ILG.Action. It realizes the discrete-to-continuum step that maps Recognition Science J-cost defects onto the Einstein tensor, thereby allowing lattice-derived curvature to enter standard general-relativity constructions.

scope and limits

used by (9)

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

depends on (9)

Lean names referenced from this declaration's body.