IndisputableMonolith.Gravity.Connection
The Gravity.Connection module supplies the metric tensor, its inverse, Christoffel symbols, and metric compatibility conditions in local coordinates for the Recognition Science gravity framework. Researchers deriving the Einstein field equations or curvature tensors cite these definitions as the starting point for coordinate-based calculations. This is a definition module containing no proofs.
claimThe metric tensor $g$ is a symmetric 4x4 matrix at each spacetime point with inverse satisfying $g g^{-1} = I$. The Christoffel symbols are given by the standard formula from metric derivatives, and metric compatibility requires the covariant derivative of $g$ to vanish.
background
This module operates in the Recognition Science gravity domain and imports the RS time quantum from Constants, where tau_0 equals 1 tick. It introduces spacetime_dim as 4, the index type Idx, MetricTensor as symmetric components, minkowski as the flat metric, ChristoffelData, christoffel_from_metric, metric_compatibility, and ConnectionCert. The local-coordinate abstraction treats the metric solely through its components, enabling downstream curvature and action definitions.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
This module provides the foundational metric and connection structures that feed into the EinsteinHilbertAction module proving Axiom 2 via Hilbert variation, the RicciTensor module defining the Einstein tensor, the RiemannTensor module, and the StressEnergyTensor module proving Axiom 3. It establishes the coordinate framework required for the Einstein field equations in the Recognition Science setting.
scope and limits
- Does not construct the full differentiable manifold structure.
- Does not prove the Bianchi identities or curvature symmetries.
- Does not include matter fields or stress-energy definitions.
- Does not specify coordinate transformations or global topology.
used by (4)
depends on (1)
declarations in this module (13)
-
def
spacetime_dim -
abbrev
Idx -
structure
MetricTensor -
structure
InverseMetric -
def
minkowski -
def
minkowski_inverse -
structure
ChristoffelData -
def
christoffel_from_metric -
theorem
christoffel_symmetric -
def
metric_compatibility -
theorem
flat_christoffel_vanish -
structure
ConnectionCert -
theorem
connection_cert