Pith. sign in
module module moderate

IndisputableMonolith.Gravity.FullEFE

show as:
view Lean formalization →

Assembles the full nonlinear 4D Einstein field equation data for Recognition Science gravity, with explicit tensor structure rather than linearized scalar placeholders. Packages Hilbert variation, matter coupling, and the vacuum EFE into a single derivation chain on the RS lattice. Gravity and QG modules cite it as the master EFE record before dark energy is attached. Structure is definitional packaging of upstream Regge, Bianchi, and Einstein-Hilbert results.

claimThe module defines full Einstein field equation data $G_{\mu\nu} = \kappa T_{\mu\nu}$ (with $\Lambda=0$) in $D=4$, recording the Einstein tensor, stress-energy, and coupling $\kappa$ explicitly as tensors. It packages Hilbert-variation and matter-coupling closures and a derivation chain from Regge calculus through the vacuum EFE on the RS lattice.

background

Recognition Science gravity replaces continuum GR scaffolding with a discrete Regge programme on the RS lattice, then recovers continuum Einstein geometry in a controlled limit. Upstream modules supply the pieces: Levi-Civita connection and Christoffel symbols in local coordinates $g:\mathbb{R}^4\to\mathbb{R}^{4\times4}$; Riemann and Ricci tensors; the Einstein-Hilbert action whose metric variation yields the Einstein tensor (Hilbert variation, Axiom 2); full nonlinear Regge calculus in place of a linearized deficit-angle ansatz; the discrete Bianchi identity (Hamber-Kagel) as the lattice analog of $\nabla^\mu G_{\mu\nu}=0$; and nonlinear/Regge convergence inputs from Regge action to Einstein-Hilbert.

Earlier linearized EFE data used scalar placeholders. This module records the tensor structure explicitly and ties constants (including RS-native units from Constants) into a single FullEFE data object and derivation chain. The vacuum sector asserts the source-free equation once the closures are in place.

proof idea

Definition and packaging module, not a single deep proof. It introduces closure records for Hilbert variation and matter coupling, a FullEFEData bundle (dimension, $\kappa$, tensor fields, cosmological constant set to zero), and a FullDerivationChain that wires Regge calculus, discrete Bianchi, Einstein-Hilbert variation, stress-energy, and convergence lemmas into the vacuum EFE statement. Individual theorems are thin assemblies or citations of upstream results (connection, curvature, EH variation, Regge convergence) rather than new analytic arguments.

why it matters in Recognition Science

This is the gravity-facing master record of the nonlinear 4D EFE inside the RS monolith before vacuum energy is restored. Downstream, FullEFEWithDarkEnergy imports it and resolves the blocker that rs_efe_data carries cosmological_constant = 0, inserting a nonzero, forced, covariantly conserved vacuum term into the QG/EFE chain.

In the broader framework it sits after the discrete gravity stack (Regge, Bianchi, EH action) and before cosmology-facing extensions. It makes the tensorial EFE, not a linearized proxy, the object that zero-parameter gravity and later dark-energy work must match. Landmarks touched indirectly: continuum limit of the discrete programme and conservation via discrete Bianchi, not the T0-T8 forcing chain itself.

scope and limits

used by (1)

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

depends on (11)

Lean names referenced from this declaration's body.

declarations in this module (20)