Synchronous coordinates for irrotational dust (source code)

= Synchronous coordinates for irrotational dust
{title2=$u^\flat=-dt,\quad g=-dt^2+g_{ij}dx^idx^j$}

For <relativistic dust> with nowhere-zero <density>, <stress-energy conservation> implies zero <four-acceleration>. If its normalized <four-velocity> $u$ has <hypersurface orthogonality>, then $u^\flat\wedge du^\flat=0$ and $\iota_u du^\flat=0$. The <interior product> of the first identity gives $du^\flat=0$. The <Poincaré lemma> supplies $u^\flat=-dt$ locally; spatial <coordinate functions> constant along the <smooth flow> of $u$ give $u=\partial_t$, $g_{tt}=-1$ and $g_{ti}=0$. The resulting <synchronous coordinates> describe the dust until the local coordinate construction fails.