gamma_pot
plain-language theorem explainer
This definition supplies a constant placeholder for the gamma potential in the parametrized post-Newtonian expansion of the ILG model. Researchers constructing metric potentials from scalar fields in modified gravity would cite it during early scaffolding of PPN coefficients. The implementation is a direct constant assignment returning unity independent of inputs.
Claim. The gamma potential is the constant function returning 1, written $gamma_{pot}(psi, p) := 1$, where $psi$ denotes a scalar field and $p$ is the parameter bundle holding the coupling strength alpha together with the lag constant.
background
The ILG parameter structure is a bundle containing two real numbers: alpha for coupling strength and cLag for the lag term. RefreshField is an alias for the scalar field type. This declaration sits inside the potential-based PPN definitions, whose module comment states the intent to express the metric potentials Phi and Psi from the supplied scalar field and parameters.
proof idea
The definition is a direct constant assignment of the real number 1, with no lemmas, tactics, or reductions applied.
why it matters
It provides the initial scaffold for the gamma potential inside the ILG PPN module, preparing the ground for sibling definitions of the full gamma and beta coefficients. The placeholder connects the action module's parameter and field structures to observable post-Newtonian limits. In the Recognition Science setting it supports the eventual derivation of constants such as the fine-structure value inside the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.