IndisputableMonolith.Relativity.ILG.PPNDerive
This module supplies toy extraction formulas for the PPN parameters gamma and beta, kept local inside the ILG layer. Researchers working on parametrized post-Newtonian expansions inside Recognition Science would cite it to avoid pulling in the full PostNewtonian stack. The module replaces an earlier trivial Prop := True stub with a small, honest certificate built from the upstream PPN potential definitions.
claimExtraction formulas $\gamma = \gamma(\Phi,\Psi)$ and $\beta = \beta(\Phi,\Psi)$ together with the certificate PPNDerivationHolds.
background
The module sits inside the Relativity.ILG layer and imports only the sibling PPN module. That upstream module supplies potential-based PPN definitions (scaffold): use Φ, Ψ from ψ and params. The local doc comment states the intent explicitly: "Toy extraction formulas for PPN parameters. We intentionally keep these local to the ILG layer (rather than importing the full PostNewtonian stack) to avoid creating heavy dependency edges from Relativity.lean. The point of this file is to eliminate the previous Prop := True stub with a small, honest certificate."
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the concrete certificate that replaces the earlier stub, thereby allowing the Relativity layer to reference PPN parameters without importing the full PostNewtonian machinery. It feeds the main Relativity module by providing the local gamma and beta extraction formulas listed among its siblings.
scope and limits
- Does not import the full PostNewtonian stack.
- Does not create heavy dependency edges from Relativity.lean.
- Does not supply a complete PPN formalism.
- Does not claim to derive the parameters from first principles outside the ILG scaffold.