PPNParameters
plain-language theorem explainer
PPNParameters packages the two post-Newtonian parameters γ and β as real numbers for insertion into the 1PN metric. Workers constructing parametrized expansions of the spacetime metric cite this record when assembling g_00, g_0i and g_ij components from potentials. The definition is a direct structure with two fields of type real and carries no computational content.
Claim. The parametrized post-Newtonian parameters consist of a pair of real numbers $γ, β ∈ ℝ$.
background
The module develops the post-Newtonian expansion of the metric in terms of Newtonian potentials. PPNParameters supplies the two free parameters that multiply those potentials in the standard 1PN line element. Upstream definitions of γ appear as the Euler-Mascheroni constant and as a network exponent, while the ILG.PPN module sets both γ and β to 1 in the general-relativity limit; the present structure simply holds the symbols for later substitution.
proof idea
Direct structure definition that introduces two fields of type real.
why it matters
The structure is the parameter carrier for every 1PN metric component (g_00_1PN, g_0i_1PN, g_ij_1PN, metric_1PN and its inverse). It therefore supplies the adjustable constants that the Recognition Science post-Newtonian layer must eventually fix by matching to the underlying field equations or to the GR limit. No open question is closed here; the values remain to be determined downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.