L_density
plain-language theorem explainer
The declaration supplies a toy symbolic Lagrangian density for the ILG model expressed solely in terms of the fine-structure constant and lag parameter. Workers assembling scalar actions or testing induced-gravity scaffolds in Recognition Science cite it when the full covariant structure is not yet required. The definition is realized by direct substitution of the two parameter fields into a fixed quadratic polynomial.
Claim. The Lagrangian density is defined by the expression $L = (α^2)/2 - (c_{Lag}^2)/2 + c_{Lag}·α$, where $α$ is the fine-structure constant and $c_{Lag}$ is the lag coefficient taken from the ILG parameter bundle.
background
The Relativity.ILG.Action module re-exports geometry and field types to support construction of the ILG action. Metric is the abbreviation for the metric tensor, RefreshField stands for the scalar field, and ILGParams is the structure holding the two real parameters alpha and cLag. The upstream alpha definition from Constants.Alpha supplies the fine-structure constant as the reciprocal of its inverse.
proof idea
The definition is a direct algebraic expression that extracts the two fields from the ILGParams argument and assembles the quadratic combination without reference to the metric or field arguments.
why it matters
This supplies the placeholder Lagrangian density used to build the ILG action functional inside the relativity module. It supports the symbolic treatment of constants required by the Recognition Science forcing chain while the full covariant derivatives remain undeveloped. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.