metric_1PN_components
plain-language theorem explainer
The definition assembles the 1PN metric as a bilinear form by routing on the low indices to the appropriate component functions built from post-Newtonian potentials. Workers constructing weak-field metrics in the PPN formalism cite it to obtain the explicit g_mu nu before symmetry is imposed. The body is a direct index case dispatch that selects g_00_1PN, g_0i_1PN or g_ij_1PN according to whether the indices are zero or positive.
Claim. The 1PN metric components are the function that, given potentials and parameters, returns the value of $g_{00}^{1PN}$ when both indices are zero, $g_{0i}^{1PN}$ when one index is zero and the other positive, $g_{ij}^{1PN}$ when both are positive, and zero otherwise.
background
PPNPotentials is the structure holding the Newtonian potential U, the second-order potential U_2, and the vector potential V, each a function of the spacetime point. PPNParameters supplies the two real parameters gamma and beta that are later fixed by the field equations. BilinearForm is the interface type (Fin 4 -> R) -> (Fin 4 -> R) -> (Fin 2 -> Fin 4) -> R used for the local metric representation. The module sets the local theoretical setting as the post-Newtonian expansion of the metric in terms of these potentials. Upstream results supply the underlying potentials via the phi-ladder structures in NucleosynthesisTiers and PhiForcingDerived.
proof idea
The definition binds the low indices mu and nu, then applies a chain of if-then-else tests on whether each index equals zero or is positive. Each true branch calls the matching component function (g_00_1PN, g_0i_1PN or g_ij_1PN) with the index adjusted by subtracting one when necessary. No external lemmas are invoked; the implementation is a pure case dispatch on the four-dimensional index pair.
why it matters
This definition supplies the raw components that the parent metric_1PN wraps into a MetricTensor by pairing them with the symmetry proof metric_1PN_symmetric_proof. It therefore fills the concrete translation step from PPN potentials to an explicit metric form required for post-Newtonian equations of motion. In the Recognition framework it connects the phi-forced potentials (T5 J-uniqueness and T6 phi fixed point) to the spacetime geometry used in weak-field tests, sitting immediately before the symmetry verification that closes the 1PN construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.