Pith. sign in
module module moderate

IndisputableMonolith.Gravity.ClausiusEinsteinBridge

show as:
view Lean formalization →

Algebraic primitives for real 4×4 Lorentzian tensors used across the RS gravity stack. Supplies componentwise symmetry of covariant 2-tensors, the Minkowski metric η=diag(-1,1,1,1), quadratic contractions, null-cone predicates, and Fin-4 basis/sum helpers. Downstream modules import these to reduce Einstein-shaped matrix equations to null scalars and to build probe-independent stress. Definitional scaffolding plus elementary identities; no deep theorems.

claimThe module introduces symmetric real $4\times 4$ matrices (componentwise symmetry of covariant 2-tensors), the Minkowski metric $\eta=\mathrm{diag}(-1,1,1,1)$, the quadratic contraction $T(v,v)=\sum_{i,j} T_{ij} v^i v^j$, the Minkowski-null locus $\eta(v,v)=0$ on $\mathbb{R}^4$, Fin-4 basis vectors and finite sums, and the elementary identity that pointwise equality of tensors implies equality of their null cuts.

background

In the Recognition Science gravity program the Einstein equation is first treated algebraically, before a full dynamical geometry is installed. Real symmetric $4\times 4$ matrices stand in for covariant 2-tensors on a fixed Lorentzian 4-space with background Minkowski form $\eta=\mathrm{diag}(-1,1,1,1)$.

This module is the Fin-4 linear-algebra layer for that program: a componentwise symmetry predicate, the standard Minkowski matrix, quadratic contractions against covectors, and the null-cone predicate. These are the raw materials of the Clausius–Einstein bridge, relating thermodynamic or record-flux data to curvature-like matrices via null contractions (in the spirit of Jacobson’s thermodynamic derivation of Einstein’s equation).

Sibling definitions include the four standard basis vectors on Fin 4, finite sums over four indices, the contraction identity for $\eta$ itself, and the rewrite that pointwise tensor equality implies matching null cuts.

proof idea

This is a definition module with elementary supporting lemmas, not a theorem package. It introduces the symmetry predicate on real $4\times 4$ entries, the diagonal Minkowski matrix, the quadratic contraction map, and the zero-quadratic-form null locus. Lemmas such as the contraction identity for $\eta$ and the pointwise-equality-to-null-cut rewrite are direct unfoldings or finite-sum rewrites over Fin 4; there is no substantial proof content beyond Mathlib arithmetic.

why it matters in Recognition Science

Feeds five gravity and relativity modules that close the algebraic half of the Clausius–Einstein bridge. NullConeQuadraticTensorClass uses the null-cone and quadratic-contraction primitives to prove that values of a symmetric form on all Minkowski-null covectors determine the matrix modulo a scalar multiple of $\eta$ (Phase 5 algebraic prerequisite). RSNullFieldEquation reduces an assumed Einstein-shaped matrix equation $\kappa T=\mathrm{Ric}+f\eta$ to its null-contracted scalar form. RecordFluxStress builds a probe-independent stress matrix whose quadratic contractions are controlled for every probe. EdgeTTDecompositionLorentz4D specializes transverse-traceless decomposition to the Lorentzian null case. LocalAreaRaychaudhuri adapts matrix Ricci fields to the scalar ricciNull consumed by local area-variation equilibrium.

scope and limits

used by (5)

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

declarations in this module (16)