g_00_1PN
plain-language theorem explainer
The declaration defines the time-time component of the 1PN metric in standard parametrized post-Newtonian form. Workers in weak-field gravity and solar-system tests would cite the expression when assembling the metric tensor for comparison with observations. The body is a direct algebraic formula that substitutes the Newtonian potential and the beta parameter.
Claim. $g_{00}(x) = -(1 - 2U(x) + 2β U(x)^2)$, where $U$ is the Newtonian potential from the PPN potentials structure and $β$ is the post-Newtonian parameter from the PPN parameters structure.
background
The module constructs the post-Newtonian metric from potentials in the Recognition Science setting. The PPNPotentials structure collects the Newtonian potential function U together with a second-order potential U_2 and a vector potential V. The PPNParameters structure supplies the real numbers gamma and beta that are fixed by matching to the field equations.
proof idea
The body is a direct algebraic definition that inserts the value of the Newtonian potential U at the point x and the beta parameter into the conventional 1PN expansion for the time-time component. No lemmas are applied.
why it matters
This component is assembled into the full metric by metric_1PN_components and is invoked in the symmetry argument of metric_1PN_symmetric_proof. It supplies the 1PN metric construction step inside the post-Newtonian sector, consistent with the eight-tick octave and the forcing of D = 3 spatial dimensions from the T0-T8 chain. The value of beta remains open for determination from the field equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.