L_pot
plain-language theorem explainer
L_pot supplies the potential term in the ILG Lagrangian as half the lag coupling constant drawn from the parameter bundle. Workers constructing covariant actions for scalar-tensor models cite this term when splitting the total Lagrangian into kinetic, mass, potential, and coupling pieces. The definition is a direct parameter extraction with no further reduction.
Claim. The potential Lagrangian density is defined by $L_ {pot}(g,ψ,p)=c_{Lag}/2$, where $g$ denotes the metric tensor, $ψ$ the scalar field, and $p$ the parameter structure holding the coupling constant $c_{Lag}$.
background
The module re-exports geometry and field types for ILG constructions. Metric stands for the metric tensor. RefreshField stands for the scalar field. ILGParams is the structure bundling the parameter alpha together with the lag coupling constant cLag. The local setting is the assembly of toy covariant Lagrangians that combine Einstein-Hilbert gravity with scalar contributions.
proof idea
Direct definition that extracts and halves the cLag field of the supplied parameter structure.
why it matters
L_pot is invoked inside L_cov to complete the covariant scalar Lagrangian and inside S_total_cov to form the full action. It appears in the GR-limit theorem that recovers the Einstein-Hilbert action when both alpha and cLag vanish. Within the Recognition framework this term supplies the potential piece of the action functional used in the relativity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.