L_cov
plain-language theorem explainer
This definition assembles the covariant scalar Lagrangian for the ILG model as the algebraic sum of its kinetic, negative mass, potential, and coupling pieces. Researchers constructing modified-gravity actions or scalar-tensor theories would cite it when forming the total covariant action functional. The definition is realized as a direct one-line combination of four parameter-dependent component functions.
Claim. $L(g,ψ,p)=L_κ(g,ψ,p)−L_m(g,ψ,p)+L_V(g,ψ,p)+L_c(g,ψ,p)$, where $g$ is the metric tensor, $ψ$ the scalar field, and $p$ the parameter bundle containing the coupling constants $α$ and $c_{Lag}$.
background
The module re-exports geometry and field types for ILG use. Metric stands for the metric tensor. RefreshField stands for the scalar field. ILGParams is the structure holding the two real parameters alpha and cLag. The four component Lagrangians are defined separately: the kinetic piece equals $α^2/2$, the mass piece equals $c_{Lag}^2/2$, the potential piece equals $c_{Lag}/2$, and the coupling piece equals $c_{Lag}·α$; each component is independent of the explicit field and metric values in this toy model.
proof idea
This is a one-line definition that subtracts the mass term from the kinetic term and adds the potential and coupling terms.
why it matters
L_cov supplies the scalar-sector contribution to the total covariant action S_total_cov. It is invoked by the GR-limit theorem that recovers the Einstein-Hilbert action when both parameters vanish. The construction therefore sits inside the covariant action that connects the ILG framework to the Recognition Science forcing chain and the recovery of general relativity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.