StressEnergyCert
plain-language theorem explainer
StressEnergyCert packages the vacuum reduction of the sourced Einstein equations, the nonzero status of the RS coupling 8 phi^5, and the implication that div T vanishes whenever the Bianchi identity and EFE hold with nonzero kappa. Workers deriving conservation of energy-momentum from the Recognition framework cite this certificate when closing the matter-coupling axiom. The declaration is a plain structure that directly assembles three already-proved facts without further reduction.
Claim. A certificate structure whose fields assert: (i) if the sourced Einstein equations $G + Lambda g = kappa T$ hold with the zero stress-energy tensor, then the vacuum equations $G + Lambda g = 0$ hold; (ii) $8 phi^5 neq 0$ in $mathbb{R}$; (iii) for any $kappa neq 0$, if $nabla^mu G_{mu nu}=0$ and $nabla^mu G_{mu nu} + Lambda cdot 0 = kappa nabla^mu T_{mu nu}$, then $nabla^mu T_{mu nu}=0$.
background
The module defines the stress-energy tensor $T_{mu nu}$ via variation of the matter action and derives its conservation $nabla^mu T_{mu nu}=0$ from the contracted Bianchi identity $nabla^mu G_{mu nu}=0$ together with the Einstein field equations. Key supporting definitions are efe_with_source (the sourced equation $G_{mu nu} + Lambda g_{mu nu} = kappa T_{mu nu}$), vacuum_efe_coord (the vacuum case $G_{mu nu} + Lambda g_{mu nu}=0$), vacuum_stress_energy (the zero tensor), and Idx (the index type Fin 4). The local setting is the coordinate formulation of general relativity restricted to the Recognition Science value of the coupling kappa.
proof idea
The declaration is a structure definition with three fields. The first field is supplied by the lemma vacuum_is_special_case, the second by rs_conservation_holds (which reduces to mul_pos and pow_pos on phi), and the third by conservation_from_efe_and_bianchi. No tactics or reductions occur inside the structure itself.
why it matters
StressEnergyCert is instantiated by the theorem stress_energy_cert, which closes the conservation step of Axiom 3 (matter coupling) in the Recognition Science framework. It supplies the nonzero-kappa fact required to pass from the geometric Bianchi identity to physical conservation of energy-momentum under the specific RS coupling 8 phi^5. The construction sits inside the gravity sector that follows from the T0-T8 forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.