IndisputableMonolith.Relativity.ILG.PPN
This module scaffolds potential-based definitions for Parametrized Post-Newtonian parameters in the ILG layer, expressing gamma and beta via potentials Phi and Psi built from the field psi and model parameters. Researchers deriving local post-Newtonian observables from the ILG action cite these when avoiding the full PostNewtonian stack. The module consists solely of definitions, linear forms, and bounds with no theorems or proofs.
claimThe module defines PPN potentials $Phi$ and $Psi$ from the scalar field $psi$ and parameters, together with the parameters $gamma$ and $beta$, their linear approximations, and small-parameter bounds.
background
The module sits inside the ILG layer of Recognition Science relativity and imports geometry and field types re-exported by the Action module. Its doc-comment states: 'Potential-based PPN definitions (scaffold): use Φ, Ψ from ψ and params.' It introduces sibling definitions gamma_pot, beta_pot, gamma, beta, gamma_def, beta_def, gamma_bound, beta_bound, gamma_lin, beta_lin, gamma_bound_small, and beta_bound_small.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the local definitions consumed by the downstream PPNDerive module, which produces toy extraction formulas for PPN parameters. The downstream doc-comment notes that this keeps the ILG layer local, avoids heavy dependency edges from Relativity.lean, and replaces a prior Prop := True stub with an honest certificate.
scope and limits
- Does not derive full post-Newtonian equations of motion.
- Does not import the complete PostNewtonian stack.
- Does not prove any theorems; content is purely definitional.
- Does not address global or cosmological regimes.