IndisputableMonolith.Gravity.StressEnergyTensor
The module introduces the stress-energy tensor as the variational derivative of the matter action in local coordinates. Gravity researchers extending the Einstein equations to include sources would cite it when deriving conservation laws from the contracted Bianchi identity. It consists of abstract definitions establishing T as a symmetric tensor compatible with the metric and curvature objects imported from upstream modules.
claimThe stress-energy tensor satisfies $T_{\mu\nu} = -\frac{2}{\sqrt{-g}} \frac{\delta S_{\rm matter}}{\delta g^{\mu\nu}}$ and is represented as a symmetric $(0,2)$-tensor on the four-dimensional spacetime.
background
This module belongs to the Gravity domain and imports the RS time quantum $\tau_0 = 1$ tick from Constants, the Levi-Civita connection and Christoffel symbols in local coordinate patches from Connection, and the Ricci tensor, scalar curvature, and Einstein tensor $G_{\mu\nu}$ from RicciTensor. The upstream RicciTensor result states that $G_{\mu\nu}$ is symmetric and divergence-free. The local-coordinate setting avoids Mathlib manifold gaps while remaining rigorous for GR calculations.
The stress-energy tensor supplies the matter source term that couples to curvature in the Einstein field equations with sources.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the source term required for the Einstein field equations with matter in the Recognition Science framework. It feeds sibling declarations such as efe_with_source, conservation_from_efe_and_bianchi, and rs_conservation_holds. These in turn connect the standard GR definition of T to the divergence-free property of the Einstein tensor already established upstream.
scope and limits
- Does not derive explicit components of T for concrete matter fields.
- Does not prove the conservation equation from RS first principles.
- Does not express T in terms of the phi-ladder or J-cost.
- Does not incorporate quantum or RS-native unit corrections to T.