StressEnergy
plain-language theorem explainer
The StressEnergy structure encodes the stress-energy tensor as a symmetric map from four spacetime indices to reals. Researchers setting up the sourced Einstein field equations cite this definition when introducing the matter term on the right-hand side. It is introduced directly as a structure declaration whose only content is the component function together with the symmetry axiom.
Claim. A stress-energy tensor is a symmetric bilinear form $T: I_4 × I_4 → ℝ$ on the spacetime indices $I_4 = {0,1,2,3}$, satisfying $T_{μν} = T_{νμ}$ for all $μ,ν$.
background
The module introduces the stress-energy tensor via the standard variational definition $T_{μν} = -(2/√(-g)) δS_matter / δg^{μν}$ and then proves its conservation from the contracted Bianchi identity together with the Einstein field equations. This step establishes Axiom 3 (matter coupling) in the Recognition framework. Idx is the index type Fin 4 supplied by the Connection module; the symmetry field is the only structural requirement. Upstream dependencies include the vacuum gauge-bond configuration (Yang-MillsMassGap.vacuum) and the scalar coefficient μ from the Ndim projector, both used to anchor the zero and perfect-fluid special cases.
proof idea
Direct structure definition. The component map T and the symmetry predicate are supplied by the user of the structure; no further lemmas or tactics are applied.
why it matters
StressEnergy supplies the matter source that appears in efe_with_source, perfect_fluid and vacuum_stress_energy. It therefore completes the conservation chain stated in the module documentation: contracted Bianchi identity plus metric compatibility plus EFE imply ∇^μ T_{μν} = 0. In the broader Recognition Science setting this definition supports the gravity sector that ultimately forces D = 3 and the eight-tick octave structure. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.