S_EH
plain-language theorem explainer
S_EH aliases the Einstein-Hilbert action inside the ILG module for consistent naming across discrete-to-continuum bridges. Gravity researchers working on Regge calculus convergence cite it when equating J-cost stationarity to the standard EH form. The declaration is a direct one-line alias to EHAction, which evaluates the Ricci scalar at a fixed sample point as a placeholder for the integral.
Claim. $S_{EH} := (M_P^2/2) ∫ √(-g) R d^4x$, where the integral is replaced by a single-point Ricci scalar evaluation on the metric tensor.
background
The module re-exports geometry and field types for ILG use. EHAction defines the Einstein-Hilbert action as (M_P²/2) times the integral of √(-g) R d^4x but scaffolds it to Geometry.ricci_scalar g x₀ at the origin. Upstream results include the 'for' structure recording meta-realization properties and the volume definition as the cardinality of a vertex set.
proof idea
The definition is a one-line alias that directly assigns EHAction to S_EH.
why it matters
This alias supplies the EH action to downstream theorems including jcost_stationarity_implies_regge (equating J-cost and Regge stationarity), eh_proportional_to_R (Lagrangian density proportional to scalar curvature), and regge_to_eh_convergence_axiom. It closes the discrete-to-continuum link in the gravity chain and supports the Recognition forcing sequence from T5 J-uniqueness through T8 (D=3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.