stress_energy_cert
plain-language theorem explainer
The declaration assembles a certificate confirming conservation of the stress-energy tensor for the Recognition Science value of the coupling constant. Researchers deriving the Einstein equations with matter sources in this framework would reference it to validate the matter-coupling axiom. Its term proof directly populates the three fields of the certificate structure using lemmas on the vacuum case, the nonvanishing of eight phi to the fifth, and the conservation implication from the Bianchi identity.
Claim. The structure certifying stress-energy conservation holds, with the vacuum Einstein field equations as the zero-source special case, the coupling constant satisfying $8 phi^5 neq 0$, and the implication that the contracted Bianchi identity together with the Einstein equations forces the divergence of the stress-energy tensor to vanish whenever the coupling is nonzero.
background
The module defines the stress-energy tensor from variation of the matter action and derives its conservation from the contracted Bianchi identity combined with the Einstein field equations. This establishes Axiom 3 on matter coupling. The upstream definition of the stress-energy tensor comes from the recognition energy-momentum tensor derived from the RRF potential. The key conservation theorem states that if the Einstein field equations hold and the contracted Bianchi identity holds, then the stress-energy tensor is conserved: nabla^mu T_{mu nu} = 0. The RS-specific result shows that the coupling 8 phi^5 is nonzero.
proof idea
The proof constructs the required certificate record in term mode. It assigns the vacuum special case field directly to the corresponding vacuum theorem, sets the nonzero coupling field to the RS conservation lemma establishing eight phi to the fifth is nonzero, and defines the conservation field as the lambda abstraction that applies the general conservation from EFE and Bianchi theorem to the supplied arguments.
why it matters
This result completes the proof of Axiom 3 on matter coupling by certifying that the stress-energy tensor is conserved under the Recognition Science coupling. It sits at the end of the conservation chain that begins with the contracted Bianchi identity and the Einstein field equations. The framework uses the specific value kappa equal to eight phi to the fifth, whose positivity follows from the properties of phi. No open questions are flagged in the immediate dependencies, though the certificate may be invoked in future derivations of the field equations with sources.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.