L_coupling
plain-language theorem explainer
L_coupling supplies the interaction term in the ILG scalar Lagrangian as the product of the lag coupling constant and the fine-structure constant. Researchers building covariant actions in the ILG toy model cite this term when summing kinetic, mass, potential, and coupling pieces into L_cov. The definition is a direct parameter multiplication drawn from the ILGParams bundle with no additional computation or dependence on metric or field arguments.
Claim. The coupling Lagrangian density is defined by $L_mathrm{coupling}(g,psi,p)=c_mathrm{Lag}cdotalpha$, where $p$ is the parameter bundle containing the fine-structure constant $alpha$ and the lag coupling $c_mathrm{Lag}$, while the metric $g$ and scalar field $psi$ are unused in this term.
background
The ILG.Action module re-exports geometry and field types for constructing the ILG Lagrangian. Metric abbreviates Geometry.MetricTensor and RefreshField abbreviates Fields.ScalarField. ILGParams is the structure that bundles two real parameters: alpha (the fine-structure constant) and cLag (the lag coupling constant). Upstream, alpha is supplied by Constants.Alpha as the reciprocal of alphaInv. This definition appears alongside the sibling terms L_kin, L_mass, and L_pot that are added to produce L_cov.
proof idea
The declaration is a direct definition that extracts the two fields of the ILGParams structure and returns their product. No lemmas or tactics are invoked; it is a one-line parameter multiplication.
why it matters
L_coupling is referenced by L_cov to form the full covariant scalar Lagrangian and by the theorem gr_limit_cov that recovers the Einstein-Hilbert action when both alpha and cLag are set to zero. It inserts the fine-structure constant into the toy ILG action, consistent with the Recognition Science placement of alpha inverse in the narrow interval (137.030, 137.039). No open questions are closed by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.