perfect_fluid
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.