Pith. sign in
module module high

IndisputableMonolith.Gravity.Connection

show as:
view Lean formalization →

The Gravity.Connection module defines the metric tensor as a symmetric 4x4 matrix and associated connection objects for spacetime in Recognition Science gravity. It is imported by the Einstein-Hilbert action, Ricci tensor, Riemann tensor, and stress-energy tensor modules. The module consists entirely of definitions with no proofs.

claimA metric tensor $g_{\mu\nu}$ is a symmetric 4x4 matrix at each spacetime point, with Christoffel symbols $\Gamma^\lambda_{\mu\nu}$ derived from it via the standard formula and satisfying metric compatibility.

background

This module belongs to the gravity domain and imports the Constants module, whose doc states that the fundamental RS time quantum is $\tau_0 = 1$ tick. It introduces sibling definitions including MetricTensor (symmetric matrix components), InverseMetric, ChristoffelData, christoffel_from_metric, metric_compatibility, and ConnectionCert. The local setting is a coordinate-based abstraction of differential geometry for gravity, with spacetime_dim and Idx as indexing primitives.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Definitions here supply the metric and connection primitives required by the EinsteinHilbertAction module (which proves Axiom 2 via Hilbert variation), the RicciTensor module (which defines the Einstein tensor), the RiemannTensor module (which defines curvature and the Bianchi identity), and the StressEnergyTensor module (which proves Axiom 3 on matter coupling and conservation).

scope and limits

used by (4)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)