PPNPotentials
plain-language theorem explainer
PPNPotentials is the structure that packages the three post-Newtonian potentials U, U_2 and V required to assemble the 1PN metric in Recognition Science. Workers constructing explicit 1PN line elements or checking inverse-metric identities cite this record when passing potentials into the component functions g_00_1PN, g_0i_1PN and g_ij_1PN. The declaration is a bare structure definition with no reduction or proof obligations.
Claim. A record $PPNPotentials$ whose fields are scalar functions $U,U_2:ℝ^4→ℝ$ and a vector function $V:ℝ^4→ℝ^3$, supplying the Newtonian, quadratic-scalar and gravitomagnetic potentials that enter the first post-Newtonian metric.
background
In the post-Newtonian sector the metric is written to O(ε²) using the standard PPN potentials. The imported Relativity.Geometry supplies the MetricTensor and ContravariantBilinear types while Calculus provides the index operations. RS-native units fix c=1, so the potentials are dimensionless and the coordinate x:Fin 4→ℝ already incorporates the gauge τ₀=1 tick, ℓ₀=1 voxel. Upstream definitions such as the inflaton V and the spectral V are unrelated name collisions; the relevant prior result is the RSUnits gauge that normalizes all subsequent expansions.
proof idea
The declaration is a structure definition; Lean simply records the three field types with no tactics or lemmas applied.
why it matters
PPNPotentials supplies the input data for every 1PN metric constructor (metric_1PN, inverse_metric_1PN, g_00_1PN, …) and for the symmetry and inverse-correctness theorems that follow. It therefore occupies the exact slot between the general Recognition forcing chain and the concrete post-Newtonian limit, allowing the framework to recover the standard GR 1PN form once the PPN parameters γ and β are fixed by the field equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.