gr_limit_reduces
plain-language theorem explainer
The theorem establishes that the full ILG action equals the Einstein-Hilbert action exactly when the lag coupling and alpha parameter are both zero. Researchers deriving the general-relativity limit of the ILG model would cite this reduction. The proof proceeds by direct unfolding of the composite action definitions followed by simplification on the kinetic and potential integrals.
Claim. Let $S(g,ψ;C_{lag},α)$ denote the full ILG action and $S_{EH}(g)$ the Einstein-Hilbert action. Then $S(g,ψ;0,0)=S_{EH}(g)$.
background
Metric is the abbreviation for the spacetime metric tensor. RefreshField stands for the scalar field ψ. The full action S is defined as the sum of the Einstein-Hilbert term S_EH and the ψ-sector PsiAction, which splits into kinetic and potential contributions. Upstream kinetic_action supplies the integral (1/2)∫√(-g) g^{μν}(∂_μψ)(∂_νψ)d⁴x while potential_action supplies the corresponding mass term integral.
proof idea
The proof unfolds S together with PsiAction, PsiKinetic and PsiPotential, then applies simp using the kinetic_action and potential_action lemmas from the Fields.Integration module.
why it matters
This reduction is invoked directly by the bundled-parameter theorem gr_limit_on. It supplies the GR-limit step inside the ILG action construction, confirming consistency with Einstein-Hilbert gravity when the Recognition-Science lag coupling vanishes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.