g_ij_1PN
plain-language theorem explainer
g_ij_1PN supplies the spatial components of the 1PN metric in parametrized post-Newtonian form, returning 1 plus twice gamma times the Newtonian potential U(x) precisely when the indices i and j coincide and are spatial, and zero otherwise. Workers assembling weak-field expansions or testing general relativity via PPN parameters cite this helper when building the full metric tensor. The definition is realized as a direct index-conditional expression with no further computation.
Claim. $g_{ij}(x) = 1 + 2 gamma U(x)$ when $i = j > 0$ and $0$ otherwise, where $U$ is the Newtonian potential from the PPNPotentials structure and gamma is the PPN parameter from PPNParameters.
background
The module constructs post-Newtonian potentials for the 1PN metric. PPNPotentials is a structure containing the Newtonian potential function U together with the second-order scalar U_2 and the vector potential V. PPNParameters holds the adjustable coefficients gamma and beta that are later fixed by the field equations. The local setting is the explicit component definitions that precede wrapping into the MetricTensor bilinear form supplied by the Gravity.Connection and Foundation.Hamiltonian modules. Upstream results include the RS-native units definition and the Euler-Mascheroni constant, though the gamma appearing here is the distinct PPN parameter.
proof idea
The definition is a one-line conditional expression on the indices i and j that scales the potential only on the spatial diagonal.
why it matters
This component is used by metric_1PN_components to assemble the full bilinear form and by metric_1PN_symmetric_proof to establish symmetry. It encodes the standard spatial 1PN metric in PPN form, consistent with the Recognition Science gravity connection and the requirement that the metric reduce to the Minkowski background at zeroth order. No open questions are attached at this definition level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.