Pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry

show as:
view Lean formalization →

Barrel module assembling the continuum geometry stack for Recognition Science relativity: manifolds, metrics, connections, curvature, Levi-Civita uniqueness, parallel transport, and the discrete-to-continuum J-cost bridge. Downstream field and ILG action modules import it as a single entry point. Structure is re-export only; proofs live in the child files, several of which remain scaffolds.

claimThe geometry layer for RS relativity: a pseudo-Riemannian spacetime $(M,g)$ with Christoffel connection $\Gamma^\rho_{\mu\nu}$, curvature (Ricci, Einstein tensor), the unique torsion-free metric-compatible $\nabla$, parallel transport, and a bridge from lattice $J$-cost defects to continuum $\nabla^2$ and the Einstein field equations.

background

Recognition Science builds continuum GR from a discrete lattice whose cost is the $J$-functional $J(x)=(x+x^{-1})/2-1$. This module is the import hub for that continuum side. Child files supply a typed manifold placeholder, tensor and metric types, Christoffel symbols and covariant derivatives, curvature tensors, metric unification, the fundamental theorem of pseudo-Riemannian geometry (unique torsion-free metric-compatible connection), parallel transport, and DiscreteBridge.

DiscreteBridge is the conceptual spine: lattice $J$-cost $\to$ quadratic defect $\to$ lattice Laplacian $\to \nabla^2 \to$ Ricci scalar $\to$ Einstein tensor $\to$ EFE. Manifold and Connection are explicitly marked scaffold: not in the certificate chain; Christoffel symbols may default to zero there. LeviCivitaTheorem states existence and uniqueness of $\nabla$ with coefficients as in Curvature, and records torsion-freeness via christoffel symmetry.

proof idea

This is a definition and re-export module, not a proof unit. It imports nine geometry submodules and exposes their API. Substantive arguments live downstream of the imports: LeviCivitaTheorem for uniqueness of the metric connection, Curvature for Christoffel construction from $g$, and DiscreteBridge for the lattice-to-EFE chain. Scaffold children (Manifold, Connection) contribute typed placeholders only.

why it matters in Recognition Science

Fields.Integration, Fields.Scalar, and ILG.Action all import this hub, so every continuum field integral, scalar assignment, and ILG action functional depends on the geometry stack assembled here. It is the continuum counterpart to the discrete RS lattice and the place where $D=3$ spacetime structure and curvature enter the relativity domain. DiscreteBridge ties lattice $J$-cost directly to the Einstein tensor, linking the forcing-chain geometry (T8 spatial dimensions, eight-tick structure upstream) to classical GR. Several imported files remain scaffolds, so certificate strength is limited to the proved fragments (e.g. christoffel symmetry, Levi-Civita uniqueness claims) until those placeholders are discharged.

scope and limits

used by (3)

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.