IndisputableMonolith.Gravity.Connection
The Gravity.Connection module supplies the metric tensor as a symmetric 4x4 matrix in local coordinates together with the induced Christoffel symbols and compatibility conditions. It serves as the coordinate foundation for all subsequent curvature and action calculations in the Recognition Science gravity development. Physicists deriving the Einstein tensor or stress-energy conservation cite it for the explicit Levi-Civita connection data. This is a definition module containing no proofs.
claimLet $g_{ab}$ be a symmetric $(0,2)$-tensor on a 4-dimensional spacetime with inverse $g^{ab}$. The Christoffel symbols are defined by $Γ^c_{ab} = ½ g^{cd}(∂_a g_{bd} + ∂_b g_{ad} - ∂_d g_{ab})$, satisfying metric compatibility $∇_c g_{ab} = 0$ and vanishing on the Minkowski background.
background
The module opens with the RS-native time quantum τ₀ = 1 tick imported from Constants. It introduces spacetime_dim = 4, an index type Idx, the MetricTensor as a symmetric 4×4 matrix of components at each point, its inverse, the flat Minkowski metric, and the ChristoffelData record. These objects are used to construct christoffel_from_metric, the symmetry lemma christoffel_symmetric, metric_compatibility, and the flat_christoffel_vanish statement. The supplied module doc-comment states that the metric is abstracted simply as its components.
proof idea
This is a definition module, no proofs. It consists of type and structure definitions for MetricTensor, InverseMetric, ChristoffelData together with the explicit formula christoffel_from_metric and the three supporting lemmas that record symmetry, compatibility, and flat-space vanishing.
why it matters in Recognition Science
The module supplies the connection data required by EinsteinHilbertAction (which proves Axiom 2 via Hilbert variation), RicciTensor (which builds the Einstein tensor from the Riemann tensor), RiemannTensor (which defines curvature from Christoffel symbols), and StressEnergyTensor (which proves Axiom 3 via conservation). It therefore anchors the entire coordinate-based gravity chain that recovers the Einstein field equations from the Recognition Science forcing chain.
scope and limits
- Does not introduce a differentiable manifold structure or coordinate charts.
- Does not define the Riemann or Ricci tensors.
- Does not treat matter fields or the stress-energy tensor.
- Does not prove the Bianchi identities or divergence-free property of the Einstein tensor.
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