pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Relativity.PostNewtonian.Metric1PN

show as:
view Lean formalization →

The Metric1PN module supplies the post-Newtonian potentials together with the explicit 1PN metric components in the Recognition Science relativity setting. Researchers deriving solar-system orbits or light propagation at order 1/c^2 would import these objects. The module is a pure definition collection that re-exports geometry and calculus primitives without internal theorems.

claimThe 1PN metric is $g_{00} = -1 + 2U + O(c^{-4})$, $g_{0i} = -4V_i + O(c^{-5})$, $g_{ij} = (1 + 2U)δ_{ij} + O(c^{-4})$, where $U$, $V_i$ are the PPN potentials and the coefficients are controlled by the PPN parameters.

background

This module sits inside the post-Newtonian sector of Recognition Science relativity. It depends on the Geometry aggregator, which re-exports spacetime structure, and the Calculus aggregator, which supplies the differential operators needed for the potentials. The central objects are PPNPotentials (the Newtonian and gravitomagnetic potentials) and PPNParameters (the set of coefficients that reduce to GR values when the underlying J-equation is satisfied).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the 1PN metric components and their inverse that are required by any higher-order post-Newtonian calculation. It therefore feeds the constructions metric_1PN, inverse_metric_1PN and PPNInverseFacts inside the same file, completing the first step of the weak-field expansion that follows from the Recognition Science forcing chain.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)