pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Relativity.ILG.Action

show as:
view Lean formalization →

This module aggregates and re-exports geometry and field types for the Induced Lattice Gravity (ILG) framework. Researchers deriving gravitational actions from lattice structures would import it to access metric, volume, and action definitions without separate upstream calls. It functions as a thin aggregator module containing no internal proofs or new objects.

claimThe module re-exports the metric tensor $g$, volume element, Einstein-Hilbert action $S_{EH}$, and field actions for the ILG model in Recognition Science.

background

In Recognition Science, gravity emerges from the J-cost and phi-ladder constructions. This module sits in the Relativity.ILG namespace and imports from IndisputableMonolith.Relativity.Geometry, whose doc states it 're-exports all geometry components for convenient importing,' and from IndisputableMonolith.Relativity.Fields, which 'Re-exports all field-related definitions.' It exposes sibling definitions including Metric, EHAction, S_EH, PsiAction, and ILGParams.

proof idea

This is a definition module, no proofs. It consists only of three import statements that aggregate upstream Geometry and Fields modules for ILG use.

why it matters in Recognition Science

This module supplies the action primitives that feed into IndisputableMonolith.Relativity.ILG.PPN for potential-based PPN definitions and IndisputableMonolith.Relativity.ILG.Substrate for the Quantum Bridge connection. It supports the ILG framework's derivation of gravitational dynamics from the Recognition Science forcing chain (T0-T8) and RCL.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (34)