g_0i_1PN
plain-language theorem explainer
This definition supplies the explicit 0i component of the 1PN metric tensor as a scaled vector potential. Researchers constructing post-Newtonian expansions or verifying metric symmetry in the Relativity.PostNewtonian module cite it directly. The implementation is a one-line algebraic expression that multiplies the i-th component of pots.V by the prefactor -(4*gamma + 3)/2.
Claim. The off-diagonal metric component at first post-Newtonian order is given by $g_{0i}(x) = -((4γ + 3)/2) V_i(x)$, where $γ$ is the PPN parameter and $V_i$ is the corresponding component of the vector potential.
background
The module assembles post-Newtonian potentials into a metric. PPNPotentials is the structure holding the Newtonian potential U, its quadratic correction U_2, and the vector potential V that maps a point in Fin 4 to a vector in Fin 3. PPNParameters holds the two real scalars gamma and beta that are later fixed by the field equations. This definition is one of four component functions (g_00_1PN, g_0i_1PN, g_ij_1PN) that feed metric_1PN_components. Upstream, the ILG.PPN module defines gamma as identically 1 in the GR limit.
proof idea
One-line definition that evaluates the expression -(4 * params.gamma + 3) / 2 multiplied by the i-th component of pots.V x.
why it matters
It supplies the 0i block required by metric_1PN_components to build the full BilinearForm and by metric_1PN_symmetric_proof to verify g_μν = g_νμ. Within Recognition Science the construction embeds the post-Newtonian limit of the metric derived from the J-cost functional, consistent with D = 3 spatial dimensions and the eight-tick octave. It leaves open the dynamical determination of gamma and beta from the underlying field equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.