metric_1PN
plain-language theorem explainer
The definition assembles the standard 1PN metric tensor from post-Newtonian potentials and parameters. Workers in post-Newtonian relativity cite it when constructing the weak-field metric expansion in PPN form. The construction is a direct record definition that populates the component map and attaches the symmetry condition.
Claim. Let $U, U_2, V$ be the post-Newtonian potentials and let $gamma, beta$ be the PPN parameters. The 1PN metric tensor is the symmetric bilinear form whose components are assembled from these quantities.
background
Post-Newtonian potentials are encoded in the structure containing the scalar potentials $U$ and $U_2$ together with the vector potential $V$. The parameters structure holds $gamma$ and $beta$ to be fixed by the field equations. The target type MetricTensor is the local interface consisting of a component function together with a symmetry proof; upstream definitions of this interface appear in the Gravity.Connection and Hamiltonian modules.
proof idea
The definition is a one-line wrapper that applies the component construction to populate the metric field and attaches the symmetry proof.
why it matters
This definition supplies the metric used by the inverse correctness theorem and the PPN inverse facts class. It completes the standard 1PN metric construction step in the post-Newtonian expansion. It interfaces with the MetricTensor type appearing in gravity connection and Hamiltonian modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.