pith. sign in
module module moderate

IndisputableMonolith.Relativity.PostNewtonian.Metric1PN

show as:
view Lean formalization →

This module collects definitions for post-Newtonian potentials and the first post-Newtonian metric components. Researchers deriving weak-field gravity expansions or PPN parameters would reference these objects. The module is a pure collection of definitions and supporting statements with no central theorem or proof.

claimThe 1PN metric is expressed via Newtonian and post-Newtonian potentials $U$, $V_i$, $W_{ij}$ together with PPN parameters $eta$, $\gamma$ as $g_{00} = -1 + 2U + ext{higher terms}$, $g_{0i} = -4V_i$, $g_{ij} = (1+2U)\\,\delta_{ij}$.

background

The module sits inside the post-Newtonian sector of the relativity development. It imports the Calculus aggregator for differentiation tools and the Geometry aggregator for re-exported geometric primitives. Its sibling declarations introduce PPNPotentials, PPNParameters, the individual metric components $g_{00_1PN}$, $g_{0i_1PN}$, $g_{ij_1PN}$, and the assembled metric_1PN object.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the concrete 1PN metric expressions required by the parameterized post-Newtonian formalism. It directly supports the sibling declarations metric_1PN, ppn_GR and PPNInverseFacts inside the same file.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)