L_mass
The definition supplies the mass term in the ILG scalar Lagrangian as half the square of the lag coupling constant drawn from the parameter bundle. Workers assembling covariant actions or taking the GR limit cite this term when summing Lagrangian pieces. It is realized as a direct one-line assignment that discards the metric and field arguments.
claimThe mass term is defined by $L_mathrm{mass}(g, psi, p) = (p.c_mathrm{Lag})^2 / 2$, where $g$ is a metric tensor, $psi$ a scalar field, and $p$ the ILG parameter structure containing the lag coupling constant.
background
The ILG.Action module re-exports geometry and field types for constructing the induced Lagrangian gravity action. Metric aliases Geometry.MetricTensor, RefreshField aliases Fields.ScalarField, and ILGParams is the structure bundling alpha and cLag. Upstream results include the constant scalar field definition providing a baseline configuration and the and theorem from CirclePhaseLift that supplies explicit log-derivative bounds for related analytic work.
proof idea
This is a direct definition returning (p.cLag ^ 2) / 2. No lemmas are applied and the metric and refresh field inputs are ignored.
why it matters in Recognition Science
It supplies the mass piece to L_cov, which assembles the total covariant action and enables the gr_limit_cov theorem that recovers the Einstein-Hilbert action when alpha and cLag vanish. The definition fills the placeholder for the potential Lagrangian scaled by field variance in the ILG framework.
scope and limits
- Does not depend on the metric tensor configuration.
- Does not depend on the refresh field values.
- Does not include kinetic or potential contributions.
- Does not enforce covariance or field equations.
formal statement (Lean)
74noncomputable def L_mass (_g : Metric) (_ψ : RefreshField) (p : ILGParams) : ℝ := (p.cLag ^ 2) / 2
proof body
Definition body.
75/-- Potential Lagrangian - depends on metric and refresh field configuration.
76 Placeholder using coupling constant scaled by field variance. -/