metric_1PN_symmetric_proof
plain-language theorem explainer
Symmetry of the 1PN metric components under index interchange holds for any post-Newtonian potentials and parameters. Researchers constructing post-Newtonian expansions in general relativity cite this to confirm that the assembled metric tensor satisfies the necessary symmetry condition. The proof proceeds by exhaustive case analysis on the sixteen index pairs in four-dimensional spacetime, reducing each branch via unfolding and simplification.
Claim. Let $U$, $U_2$, and $V$ be the post-Newtonian potentials and let $gamma$, $beta$ be the PPN parameters. Then the 1PN metric components obey $g_{mu nu}(x) = g_{nu mu}(x)$ for every spacetime point $x$, where the components are assembled from the standard 1PN expressions involving these potentials and parameters.
background
The post-Newtonian framework expands the metric to first order in the Newtonian potential. PPNPotentials is the structure collecting the scalar potentials $U$ and $U_2$ together with the vector potential $V$. PPNParameters holds the two free parameters $gamma$ and $beta$ that are later fixed by matching to the field equations. The local module develops the 1PN metric in standard PPN form. Upstream component functions supply the explicit expressions for $g_{00}$, $g_{0i}$, and $g_{ij}$ that enter the definition of the full metric components.
proof idea
The proof introduces the indices $mu$ and $nu$ extracted from the low function, then performs case analysis on whether both are zero and whether the first is zero while the second is positive. For the remaining cases it applies fin_cases on both indices and reduces each of the sixteen branches by unfolding the component definitions and simplifying with the explicit forms of $g_{00}$, $g_{0i}$, and $g_{ij}$.
why it matters
This result is invoked directly by the definition of the full 1PN metric tensor, which packages the components together with the symmetry proof. It completes the construction of a symmetric metric in the post-Newtonian approximation, consistent with the requirements of a Lorentzian metric in four-dimensional spacetime. The parent construction appears in the same module and supplies the metric object used in subsequent post-Newtonian calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.