StressEnergyTensor
plain-language theorem explainer
The recognition energy-momentum tensor is assembled from the first derivatives of the RRF potential contracted against the metric and its inverse. Researchers deriving conservation laws inside the Recognition Hamiltonian cite this construction when coupling the field to gravity. The body directly transcribes the canonical massless-scalar expression without invoking auxiliary lemmas.
Claim. For recognition field potential $ψ$ and metric $g$, the bilinear form $T_{μν}$ is given by $∂_μψ ∂_νψ - (1/2) g_{μν} g^{αβ} ∂_αψ ∂_βψ$.
background
The module derives the recognition Hamiltonian for the RRF, an interface mapping four-dimensional coordinates to real values. MetricTensor supplies the metric components while BilinearForm is the target type for symmetric rank-2 tensors. The partial derivative accessor and inverse-metric function are sibling definitions that extract the kinetic terms needed for the expression.
proof idea
The definition is a direct encoding of the scalar-field stress-energy formula. It projects the indices μ and ν from the low argument, forms the product of partial derivatives, and subtracts the trace term obtained by contracting with the inverse metric.
why it matters
This definition is invoked by the stress_energy_cert theorem to certify that energy-momentum conservation follows from time-translation invariance of the metric. It supplies the source term that links the RRF potential to the gravitational sector, consistent with the module goal of obtaining conservation from symmetry in the Recognition Hamiltonian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.