L_kin
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not depend on the metric tensor or scalar field values.
- Does not include mass, potential or coupling contributions.
- Does not perform integration or covariant operations.
- Does not encode any dynamics beyond the constant alpha term.
formal statement (Lean)
73noncomputable def L_kin (_g : Metric) (_ψ : RefreshField) (p : ILGParams) : ℝ := (p.alpha ^ 2) / 2