inverse_metric_1PN
plain-language theorem explainer
The definition supplies the contravariant components of the 1PN metric tensor expressed through the PPN potentials U and V together with the parameters γ and β. Workers deriving equations of motion or checking consistency of the post-Newtonian expansion in Recognition Science cite this construction when raising indices on the metric. The body is a direct index-by-index case distinction that assigns the appropriate algebraic combination of potentials to each (μ, ν) slot.
Claim. The inverse metric components at 1PN order are given by the contravariant bilinear form whose entries read: $g^{00} = -(1 + 2U + 2(2β-1)U^2)$, $g^{0i} = g^{i0} = ((4γ+3)/2) V^i$, $g^{ij} = δ^{ij}(1-2γ U)$ (off-diagonal spatial entries zero), where U and V are the supplied PPN potentials and γ, β are the PPN parameters.
background
The module works in the post-Newtonian regime where the metric is expanded to order ε³. PPNPotentials is the structure carrying the Newtonian scalar potential U, its quadratic correction U₂, and the vector potential V whose components are indexed by Fin 3. PPNParameters holds the two real numbers γ and β that remain free until fixed by the underlying field equations. The local setting is therefore the standard parametrized post-Newtonian form of the metric and its inverse. Upstream the ContravariantBilinear type from the geometry module supplies the tensor signature used as the return type.
proof idea
The definition is a direct case analysis on the pair of indices (μ, ν). The time-time slot receives the quadratic expression in U; each time-space slot pulls the matching component of V and multiplies by (4γ+3)/2; the spatial block is diagonal with entries 1-2γU. No auxiliary lemmas are invoked; the construction is purely by pattern matching on the Fin 4 indices.
why it matters
The definition is required by the theorem inverse_1PN_correct, which verifies that the product of metric_1PN and inverse_metric_1PN recovers the Kronecker delta to numerical tolerance 0.001, and by the class PPNInverseFacts that packages the same statement. It therefore closes the algebraic consistency check for the 1PN inverse in the Recognition Science post-Newtonian development. The construction implements index raising at the first post-Newtonian level once the potentials have been obtained from the J-cost function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.