S_total_cov
S_total_cov assembles the total covariant action for the ILG scalar model as the direct sum of the Einstein-Hilbert term and the covariant Lagrangian. Researchers deriving GR limits or varying the action in Recognition Science relativity would cite this definition. The construction is a one-line algebraic sum that delegates all content to the already-defined S_EH and L_cov.
claimThe total covariant action is given by $S_{total,cov}(g,ψ,p) := S_{EH}(g) + L_{cov}(g,ψ,p)$, where $g$ is a metric tensor, $ψ$ a scalar field, and $p$ the parameter structure holding the real numbers $α$ and $C_{lag}$.
background
The ILG.Action module re-exports geometry and field types for the Indisputable Logic Gravity construction. Metric is the Geometry.MetricTensor, RefreshField is the Fields.ScalarField, and ILGParams is the structure containing the real parameters alpha and cLag. L_cov expands to the sum of kinetic, mass, potential, and coupling contributions, while S_EH is an alias for the Einstein-Hilbert action. Upstream, C_lag is fixed at $φ^{-5}$ by the eight-tick resonance definition, and the for structure records the meta-realization properties required by self-reference axioms.
proof idea
This is a one-line definition that returns the sum S_EH g + L_cov g ψ p. No lemmas or tactics are invoked beyond the referenced definitions of S_EH and L_cov.
why it matters in Recognition Science
The definition supplies the total action specialized by the downstream theorem gr_limit_cov to the pure Einstein-Hilbert case when alpha and cLag are set to zero. It realizes the covariant extension of the action inside the Recognition Science framework, consistent with the eight-tick octave and the phi-ladder structure. It closes the toy scalar model before tensorial variations or full curvature corrections are introduced.
scope and limits
- Does not evaluate the spacetime integral of the Lagrangian density.
- Does not expand the explicit forms of L_kin, L_mass, L_pot, or L_coupling.
- Does not impose any coordinate chart or gauge condition.
- Does not incorporate higher-order curvature invariants beyond the Einstein-Hilbert term.
formal statement (Lean)
85noncomputable def S_total_cov (g : Metric) (ψ : RefreshField) (p : ILGParams) : ℝ :=
proof body
Definition body.
86 S_EH g + L_cov g ψ p
87
88/-- GR-limit for S_total_cov (α=0, C_lag=0). -/