gr_limit_on
plain-language theorem explainer
The theorem shows that the total ILG action on a bundled metric-field pair equals the Einstein-Hilbert action exactly when the lag coefficient and fine-structure parameter are both zero. Workers recovering classical general relativity from the ILG model would cite this to confirm the GR limit. The proof is a one-line term wrapper that unfolds the bundled definitions and applies the core reduction lemma to the unpacked components.
Claim. Let $(g,ψ)$ be a pair consisting of a metric and a RefreshField. Then the total action $S[g,ψ;α=0,C_{lag}=0]$ equals the Einstein-Hilbert action $S_{EH}[g]$.
background
ActionInputs is the abbreviation Metric × RefreshField that bundles geometric and field data for downstream action computations. S_on applies the total action S_total to such a pair, where S_total is defined as S_EH g + PsiAction g ψ p.cLag p.alpha. The upstream theorem gr_limit_reduces states that S g ψ 0 0 = S_EH g and carries the doc-comment 'GR-limit reduction: when C_lag = 0 and α = 0, the ψ-sector vanishes.' The module re-exports geometry and field types to support ILG constructions.
proof idea
The proof is a term-mode one-liner. It unfolds the definitions of S_on and S_total to expose the underlying expression, then applies the exact theorem gr_limit_reduces to the metric and field components of the input pair.
why it matters
This supplies the bundled-input form of the GR-limit reduction, ensuring the ILG action S[g,ψ;C_lag,α] recovers S_EH[g] when the ψ-sector vanishes. It closes the zero-parameter interface inside Relativity.ILG.Action and supports consistency with classical gravity in the Recognition framework, where the GR limit is recovered by setting the lag and fine-structure parameters to zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.