Pith. sign in
module module high

IndisputableMonolith.Gravity.StressEnergyTensor

show as:
view Lean formalization →

Defines the stress-energy tensor as a symmetric (0,2) source for the Einstein equation in local coordinates, together with vacuum and perfect-fluid specializations and the conservation identity that follows from the contracted Bianchi identity. Gravity and continuum-limit workers cite it when assembling the sourced EFE. The module is mostly definitional scaffolding plus short algebraic identities linking T to G.

claimThe stress-energy tensor $T_{\mu\nu}$ is the symmetric tensor obtained from matter as $T_{\mu\nu}=-(2/\sqrt{-g})\,\delta S_{\mathrm{matter}}/\delta g^{\mu\nu}$. Vacuum has $T_{\mu\nu}=0$; a perfect fluid has the standard $T_{\mu\nu}=(\rho+p)u_\mu u_\nu+p g_{\mu\nu}$. The sourced Einstein equation is $G_{\mu\nu}=8\pi G\,T_{\mu\nu}$ (RS units), and $\nabla^\mu T_{\mu\nu}=0$ follows from $\nabla^\mu G_{\mu\nu}=0$.

background

Recognition Science gravity is built in local coordinates on a smooth metric $g:\mathbb{R}^4\to\mathbb{R}^{4\times 4}$, avoiding Mathlib's missing connection API. Upstream, Connection supplies the Levi-Civita connection and Christoffel symbols; RicciTensor builds the Ricci tensor, scalar curvature, and Einstein tensor $G_{\mu\nu}$ and records that $G$ is symmetric and (stated) divergence-free.

The classical field-theory definition of stress-energy is the metric variation of the matter action. This module treats $T_{\mu\nu}$ abstractly as a symmetric tensor rather than deriving it from a concrete Lagrangian, then specializes to vacuum ($T=0$) and perfect fluid. Constants supplies the RS-native units in which the Einstein equation is written.

Conservation $\nabla^\mu T_{\mu\nu}=0$ is not postulated independently: it is the consequence of the contracted Bianchi identity once the EFE identifies $G$ with $T$.

proof idea

Definition-heavy module. Stress-energy is introduced as an abstract symmetric tensor matching the variational formula; vacuum and perfect-fluid constructors are explicit special cases. The sourced EFE is the pointwise identification $G_{\mu\nu}\propto T_{\mu\nu}$. Vacuum-as-special-case is a one-line specialization. Contracted Bianchi and conservation-from-EFE-and-Bianchi are short algebraic/identity steps: once $\nabla^\mu G_{\mu\nu}=0$ and $G\propto T$, divergence-free $T$ follows. An RS-conservation certificate packages the same identity for downstream use.

why it matters in Recognition Science

FullEFE imports this module to obtain the complete nonlinear sourced Einstein field equations from the RS discrete ledger (conditional on Regge convergence axioms). Without a stress-energy source and its conservation law, the gravity stack stops at vacuum curvature identities from RicciTensor. The module therefore closes the continuum side of the chain from ledger geometry to $G_{\mu\nu}=8\pi G,T_{\mu\nu}$ and $\nabla^\mu T_{\mu\nu}=0$, the standard GR interface that later RS mass and galactic-dynamics layers assume. It does not itself prove continuum limits; it supplies the tensorial language those limits target.

scope and limits

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (10)