gr_limit_cov
plain-language theorem explainer
When the fine-structure parameter alpha and lag coupling cLag are both zero, the covariant total action S_total_cov for a metric tensor and scalar field reduces exactly to the Einstein-Hilbert action S_EH. Researchers checking consistency between the ILG framework and classical general relativity would cite this reduction. The proof is a direct term-mode unfolding of the action and Lagrangian definitions followed by simplification.
Claim. Let $g$ be a metric tensor and $ψ$ a scalar field. Then $S_{total}^{cov}(g, ψ, {α := 0, c_{Lag} := 0}) = S_{EH}(g)$.
background
In this module Metric is an alias for the metric tensor and RefreshField for a scalar field. The total covariant action is defined as the Einstein-Hilbert action plus the covariant Lagrangian L_cov, where L_cov expands to the sum of kinetic, mass, potential, and coupling pieces. The coupling piece is exactly cLag times alpha, with alpha the fine-structure constant imported from Constants.Alpha.
proof idea
The term proof unfolds S_total_cov, L_cov, L_kin, L_mass, L_pot, and L_coupling, then applies simp. With alpha and cLag set to zero the coupling and extra terms vanish, leaving S_EH.
why it matters
This establishes the GR limit of the ILG action, confirming that the covariant formulation recovers the Einstein-Hilbert action when the extra parameters vanish. It belongs to the Relativity.ILG.Action module that re-exports geometry and fields for the ILG construction. No downstream theorems are recorded, but the result supports the framework claim that standard gravitational physics emerges in the appropriate limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.