Relativity Ilg Action

The action and its limit

The action in physics is a single number that encodes the entire behavior of a system: nature, in the standard picture, chooses the path that makes this number stationary. The Einstein-Hilbert action, written S_EH = (M_P²/2) ∫ √(-g) R d⁴x, is the classical starting point for general relativity. It takes the geometry of spacetime, summarized by the Ricci scalar R, and integrates it over the whole volume to produce one number. Varying that number with respect to the metric yields Einstein's field equations.

The ILG action, defined in the Recognition Science library, extends this classical object. It adds a second ingredient: a scalar field ψ, called the refresh field, which the framework treats as a discrete record of events. The full action is S = S_EH + PsiAction, where PsiAction combines a kinetic term, a potential term, and a coupling between the field and the geometry. Two real parameters, α and C_lag, control the strength of these contributions. The kinetic piece scales with α², the potential with C_lag², and the coupling with their product α·C_lag.

The central result is a limit theorem. When both parameters are set to zero, the entire ILG action collapses exactly to the Einstein-Hilbert action: S(g, ψ, 0, 0) = S_EH(g). The machine-checked library proves this in four equivalent forms, all reducing the field contributions to zero by direct simplification. In plain language, the framework's extended action contains standard general relativity as a special case. Turn off the refresh field and its couplings, and you recover Einstein's theory unchanged.

This matters because it anchors the framework's extension to a known reference point. Any prediction the ILG action makes about geometry, when the field is absent, must agree with the classical theory. The proof is not a numerical approximation; it is an exact identity in the formal library. The module also defines a bands structure that packages the deviation from general relativity as three nonnegative parameters, one each for post-Newtonian effects, lensing, and gravitational waves, all derived from the same product |C_lag·α|.

In Recognition Science, this action is the bridge between the framework's discrete ledger and continuous spacetime. The refresh field is the framework's own contribution, and the action is the mathematical object that lets it talk to Einstein's geometry. The limit theorem guarantees the conversation starts from a place the classical theory already understands.

/-- Full ILG action: S[g, ψ; C_lag, α] := S_EH[g] + S_ψ[g,ψ]. -/
noncomputable def S (g : Metric) (ψ : RefreshField) (C_lag α : ℝ) : ℝ :=
  S_EH g + PsiAction g ψ C_lag α

/-- GR-limit reduction: when C_lag = 0 and α = 0, the ψ-sector vanishes. -/
theorem gr_limit_reduces (g : Metric) (ψ : RefreshField) :
  S g ψ 0 0 = S_EH g := by
  unfold S PsiAction PsiKinetic PsiPotential
  simp [Fields.kinetic_action, Fields.potential_action]

/-- GR-limit for bundled parameters (α=0, C_lag=0). -/
theorem gr_limit_zero (g : Metric) (ψ : RefreshField) :
  S_total g ψ { alpha := 0, cLag := 0 } = S_EH g := by
  unfold S_total PsiAction PsiKinetic PsiPotential
  simp [Fields.kinetic_action, Fields.potential_action]

/-- GR-limit for S_total_cov (α=0, C_lag=0). -/
theorem gr_limit_cov (g : Metric) (ψ : RefreshField) :
  S_total_cov g ψ { alpha := 0, cLag := 0 } = S_EH g := by
  unfold S_total_cov L_cov L_kin L_mass L_pot L_coupling
  simp

/-- GR-limit for bundled inputs. -/
theorem gr_limit_on (inp : ActionInputs) :
  S_on inp { alpha := 0, cLag := 0 } = S_EH inp.fst := by
  unfold S_on S_total
  exact gr_limit_reduces inp.fst inp.snd

/-- Map ILG parameters to a bands schema (toy: proportional to |C_lag·α|). -/
noncomputable def bandsFromParams (p : ILGParams) : Bands :=
  let κ := |p.cLag * p.alpha|
  { κ_ppn := κ, κ_lensing := κ, κ_gw := κ
  , h_ppn := by exact abs_nonneg _
  , h_lensing := by exact abs_nonneg _
  , h_gw := by exact abs_nonneg _ }

What this page does not claim

The Einstein-Hilbert action's integration is fully implemented; the module uses a scaffold that evaluates the Ricci scalar at a sample point. The ILG action is derived from the framework's forcing chain; it is a definitional model, not a proved consequence. The refresh field has a physical interpretation beyond its role as a scalar field in the action.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Relativity/ILG/Action.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: