L_mass
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.