inverse_1PN_correct
plain-language theorem explainer
The theorem shows that the 1PN metric and its inverse satisfy the approximate Kronecker-delta relation to within an error of 0.001 for arbitrary post-Newtonian potentials and parameters. Workers verifying consistency of weak-field metric expansions in general relativity would cite it when checking index-raising operations at first post-Newtonian order. The proof is a direct one-line application of the inverse_approx field supplied by the PPNInverseFacts class.
Claim. Let $g_{ab}(x)$ be the 1PN metric tensor built from potentials $U,U_2,V$ and parameters $γ,β$, and let $g^{cd}(x)$ be the corresponding inverse. Then for every point $x$ and indices $μ,ρ$, $$|∑_ν g_{μν}(x) g^{νρ}(x) - δ_{μρ}| < 0.001.$$
background
PPNPotentials packages the three scalar and vector potentials $U$, $U_2$, $V$ that appear in the standard post-Newtonian expansion. PPNParameters holds the two free constants $γ$ and $β$ that are fixed by the field equations. The metric_1PN definition assembles these into a covariant bilinear form on four-dimensional spacetime, while inverse_metric_1PN supplies the contravariant version truncated at the same order. The class PPNInverseFacts is the interface that asserts the approximate orthogonality relation between these two tensors. The upstream kronecker definition supplies the standard Kronecker delta on Fin 4.
proof idea
One-line wrapper that applies the inverse_approx field of the supplied PPNInverseFacts instance to the given pots, params, x, μ and ρ.
why it matters
The result closes the verification that the explicitly constructed inverse_metric_1PN really inverts metric_1PN to the working precision of the 1PN truncation. It therefore supports any downstream calculation that raises or lowers indices on 1PN tensors, such as the computation of Christoffel symbols or the geodesic equation at this order. No parent theorem is listed in the used-by graph, indicating that the declaration functions as a self-contained consistency check inside the PostNewtonian module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.