PPNInverseFacts
plain-language theorem explainer
PPNInverseFacts packages the requirement that the 1PN metric and its inverse multiply to the Kronecker delta within a numerical tolerance of 0.001. Post-Newtonian expansions in general relativity cite this class to certify consistency of the approximate inverse before using it in field-equation matching. The declaration is a direct class definition with no proof body or lemmas.
Claim. The class PPNInverseFacts asserts that for all post-Newtonian potentials (with components $U$, $U_2$, $V$), parameters (with components $γ$, $β$), point $x ∈ ℝ^4$, and indices $μ,ρ ∈ {0,1,2,3}$, $$|∑_ν g_{μν}(x) g^{νρ}(x) - δ_{μρ}| < 0.001,$$ where $g$ denotes the 1PN metric tensor and $g^{νρ}$ its inverse.
background
Post-Newtonian potentials are given by the structure PPNPotentials containing the Newtonian potential $U$, second-order scalar $U_2$, and vector potential $V$. PPNParameters supplies the two free parameters $γ$ and $β$ that are later fixed by the field equations. The Kronecker delta kronecker returns 1 on equal indices and 0 otherwise. The functions metric_1PN and inverse_metric_1PN construct the covariant and contravariant tensors at first post-Newtonian order.
proof idea
The declaration is a direct class definition whose single field inverse_approx states the universal quantification and numerical bound. No upstream lemmas are invoked; the body is simply the forall statement packaged as a Prop.
why it matters
PPNInverseFacts supplies the hypothesis interface used by the theorem inverse_1PN_correct and by the stub instance ppnInverseStub. It closes the consistency check for the 1PN inverse metric inside the post-Newtonian module before higher-order corrections or exact inversion results are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.