StressEnergyTensor
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the Euler-Lagrange equation satisfied by the RRF.
- Does not incorporate additional matter fields or sources.
- Does not enforce any curvature or Einstein equation.
- Does not compute integrated totals or conserved charges.
formal statement (Lean)
64noncomputable def StressEnergyTensor (psi : RRF) (g : MetricTensor) : BilinearForm :=
proof body
Definition body.
65 fun x _ low =>
66 let μ := low 0
67 let ν := low 1
68 (partialDeriv_v2 psi μ x) * (partialDeriv_v2 psi ν x) -
69 (1/2 : ℝ) * g.g x (fun _ => 0) low * (
70 Finset.sum (Finset.univ : Finset (Fin 4)) (fun α =>
71 Finset.sum (Finset.univ : Finset (Fin 4)) (fun β =>
72 inverse_metric g x (fun i => if i.val = 0 then α else β) (fun _ => 0) *
73 (partialDeriv_v2 psi α x) * (partialDeriv_v2 psi β x)
74 )
75 )
76 )
77
78/-- **DEFINITION: Time-Translation Invariance**
79 A property of the metric and potential where they are independent of coordinate time x₀. -/