L_pot
L_pot defines the potential Lagrangian density as half the lag coupling constant drawn from the ILG parameter bundle. It supplies a constant placeholder term for the covariant scalar Lagrangian in ILG constructions. Researchers assembling total actions or verifying the GR limit would reference this term when summing Lagrangian contributions. The implementation is a direct one-line assignment with no lemmas or tactics.
claimThe potential Lagrangian density is defined by $L_mathrm{pot}(g, psi, p) := frac{c_mathrm{Lag}}{2}$, where $g$ is a metric tensor, $psi$ a scalar refresh field, and $p$ an ILG parameter structure supplying the lag coupling constant $c_mathrm{Lag}$.
background
The module re-exports geometry and field types for ILG use. Metric is an abbreviation for Geometry.MetricTensor and RefreshField for Fields.ScalarField. ILGParams is the structure bundling alpha and cLag as global parameters for the model.
proof idea
This is a direct definition that returns half the cLag component of the supplied ILGParams structure. No lemmas are invoked and the body is a simple arithmetic expression on the parameter.
why it matters in Recognition Science
L_pot supplies the potential term inside L_cov, which combines with kinetic, mass, and coupling pieces to form the covariant scalar Lagrangian. It is referenced by gr_limit_cov, where setting cLag to zero removes the term and recovers the Einstein-Hilbert action S_EH. In the ILG framework this constant term parameterizes deviations from standard gravity that vanish in the GR limit.
scope and limits
- Does not depend explicitly on the metric tensor or field configuration.
- Does not define a dynamical potential beyond the constant scaled by cLag.
- Does not relate cLag to other constants such as alpha or phi.
formal statement (Lean)
77noncomputable def L_pot (_g : Metric) (_ψ : RefreshField) (p : ILGParams) : ℝ := p.cLag / 2