gr_limit_zero
plain-language theorem explainer
The theorem shows that the total action S_total reduces exactly to the Einstein-Hilbert action S_EH when the ILG parameters alpha and cLag are both zero. Researchers deriving consistency checks between modified gravity models and classical GR would cite this result. The proof is a direct term-mode reduction that unfolds the bundled action definitions and applies simplification on the kinetic and potential integrals.
Claim. Let $g$ be a metric tensor and $ψ$ a scalar field. Then the total action $S(g, ψ, {α=0, C_{lag}=0})$ equals the Einstein-Hilbert action $S_{EH}(g)$.
background
The module re-exports geometry and field types for ILG use. Metric is an abbreviation for the metric tensor from Geometry. RefreshField is an abbreviation for the scalar field from Fields. S_total is the convenience wrapper defined as S_EH g plus PsiAction g ψ p.cLag p.alpha, where PsiAction itself splits into PsiKinetic plus PsiPotential. S_EH is an alias for the Einstein-Hilbert action EHAction. Upstream, kinetic_action computes (1/2) ∫ √(-g) g^{μν} (∂_μ ψ)(∂_ν ψ) d⁴x and potential_action computes (m²/2) ∫ √(-g) ψ² d⁴x, both using the volume element.
proof idea
Term-mode proof. It unfolds S_total, PsiAction, PsiKinetic and PsiPotential, then applies simp using the kinetic_action and potential_action definitions from Fields.Integration. No additional lemmas are invoked beyond the unfolding and the simp rules for the integrals.
why it matters
This declaration supplies the explicit GR-limit case for the bundled ILG parameters inside the relativity module. It closes the consistency requirement that the full action must recover the Einstein-Hilbert term when the extra parameters vanish, supporting the broader Recognition Science claim that the framework contains classical GR as a special case. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.