L_kin
plain-language theorem explainer
L_kin supplies the kinetic term in the ILG scalar Lagrangian as alpha squared over two. Workers assembling covariant actions in the ILG extension of general relativity cite it when building L_cov or taking the GR limit. The definition is a direct algebraic assignment that discards its metric and field arguments.
Claim. The kinetic piece of the covariant scalar Lagrangian is defined by $L_ {kin}(g,ψ,p)=α^2/2$, where $g$ denotes a metric tensor, $ψ$ a scalar field, and $p$ the parameter structure holding the fine-structure constant $α$.
background
ILGParams is the structure bundling the fine-structure constant alpha together with the lag constant cLag. Metric is the re-export of Geometry.MetricTensor and RefreshField is the re-export of Fields.ScalarField. The module itself re-exports geometry and field types for ILG use, placing this definition inside the construction of covariant scalar Lagrangians that later combine with the Einstein-Hilbert term.
proof idea
The declaration is a direct definition that returns (p.alpha ^ 2) / 2 with no lemmas or tactics applied.
why it matters
L_kin feeds L_cov, which is used by both the total covariant action and the gr_limit_cov theorem that recovers the Einstein-Hilbert action when alpha is set to zero. It supplies the tunable kinetic piece required for the ILG model to approach general relativity in the appropriate limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.