perfect_fluid
The perfect fluid stress-energy tensor takes the standard form T_mu nu equals (rho plus p) times u_mu u_nu plus p times g_mu nu, with rho the energy density, p the pressure, u the four-velocity, and g the metric. Cosmologists and relativists cite this construction when inserting matter sources into the Einstein equations. The definition is a direct algebraic assignment that satisfies the required symmetry of the stress-energy structure by ring reduction on the metric symmetry.
claim$T_{mu nu} = (rho + p) u_mu u_nu + p g_{mu nu}$, where rho is the energy density, p the pressure, u the four-velocity, and g the metric tensor.
background
StressEnergy is the structure whose T component is a symmetric bilinear map from spacetime indices to reals, obtained formally as the variation of the matter action with respect to the metric. MetricTensor supplies the symmetric bilinear form g on Idx, where Idx is the type Fin 4 labeling the four spacetime directions. The module establishes the conservation law nabla^mu T_mu nu equals zero by combining the contracted Bianchi identity on the Einstein tensor with the sourced field equations and metric compatibility.
proof idea
The definition directly populates the T field of StressEnergy with the algebraic expression (rho + p) u mu u nu + p met.g mu nu. Symmetry of the resulting tensor is discharged by a one-line tactic that invokes the metric symmetry and applies ring normalization.
why it matters in Recognition Science
This supplies the explicit matter source for the sourced Einstein field equation in the module, completing the step that proves Axiom 3 on matter coupling. It feeds the subsequent derivation of stress-energy conservation from the Bianchi identity and the field equations, placing the perfect-fluid case inside the Recognition framework's gravity sector where the stress-energy tensor enters the sourced EFE.
scope and limits
- Does not impose any equation of state relating rho and p.
- Does not enforce the normalization u_mu u^mu equals minus one.
- Does not derive the expression from a variational principle.
- Does not address coordinate covariance beyond the given indices.
formal statement (Lean)
50noncomputable def perfect_fluid (rho p : ℝ) (u : Idx → ℝ)
51 (met : MetricTensor) : StressEnergy where
52 T := fun mu nu => (rho + p) * u mu * u nu + p * met.g mu nu
proof body
Definition body.
53 symmetric := by
54 intro mu nu
55 simp [met.symmetric mu nu]
56 ring
57
58/-! ## The Einstein Field Equation with Source -/
59
60/-- The sourced EFE: G_{mu nu} + Lambda g_{mu nu} = kappa T_{mu nu}. -/