EHAction
plain-language theorem explainer
The EHAction definition supplies the Einstein-Hilbert action as a map from a metric tensor to a real scalar. Researchers assembling the ILG Lagrangian would reference this when constructing the gravitational sector of the action. The body evaluates the Ricci scalar at a fixed origin point rather than integrating over the full four-volume.
Claim. For a metric tensor $g$, the Einstein-Hilbert action is defined by $EHAction(g) := R(g)$, where $R$ is the Ricci scalar of $g$ evaluated at the origin (full spacetime integral and $M_P^2/2$ prefactor remain as scaffold).
background
The module re-exports geometry and field types for ILG use, with Metric as an abbreviation for Geometry.MetricTensor. EHAction sits inside Relativity.ILG.Action and imports Geometry to access ricci_scalar together with Fields for later coupling terms. Upstream structures from PhiForcingDerived supply the J-cost minimization that fixes the action form, while SpectralEmergence supplies the gauge content and D=3 that enter the volume element.
proof idea
The definition is a direct term-mode construction. It binds a sample point x₀ : Fin 4 → ℝ with all coordinates zero, then applies Geometry.ricci_scalar g x₀. No tactics are used; the body is a single expression that returns the scalar value at that point.
why it matters
EHAction supplies the gravitational term aliased as S_EH for the total ILG action. It fills the Einstein-Hilbert component required by the Recognition Science forcing chain (T8 fixing D=3 and the eight-tick octave) once the metric is derived from the J-cost functional. The scaffold leaves the full volume integration open, which would connect to the default_volume element defined in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.