Metric1PNSymmetricCondition
plain-language theorem explainer
Metric1PNSymmetricCondition defines the symmetry requirement for the 1PN metric tensor in the parameterized post-Newtonian expansion. Researchers in gravitational physics would reference it when verifying that the constructed metric tensor satisfies the necessary symmetry condition for spacetime. The definition consists of a direct equality check between the metric evaluated with interchanged index selectors.
Claim. Let $U, U_2, V$ be the post-Newtonian potentials and let $gamma, beta$ be the PPN parameters. The condition holds precisely when the 1PN metric tensor $g$ satisfies $g(x, 0, iota_mu) = g(x, 0, iota_nu)$ for all $x in R^4$ and indices $mu, nu in {0,1,2,3}$, where $iota$ is the index selector.
background
The module develops the post-Newtonian expansion of the metric using the parameterized post-Newtonian formalism. PPNPotentials is the structure collecting the Newtonian potential U, the second-order potential U_2, and the vector potential V. PPNParameters holds the two free parameters gamma and beta that are fixed by matching to the field equations.
proof idea
The definition is realized by direct substitution of the metric_1PN construction into the equality of the tensor evaluated at the two possible index orderings. It serves as the body for the symmetric field in the MetricTensor instance.
why it matters
This definition supplies the symmetry condition used in the construction of the 1PN metric tensor. It ensures consistency with the requirements of a pseudo-Riemannian metric in the weak-field, slow-motion limit. In the broader Recognition Science framework it contributes to the verification that the derived geometry reproduces the standard weak-field behavior of gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.