Pith. sign in
module module moderate

IndisputableMonolith.Gravity.RSNullFieldEquation

show as:
view Lean formalization →

Module developing the matrix-level RS null-field reduction: quadratic contraction of symmetric sources along null directions, Einstein-shaped sources, and the certificate that a scalar metric term is invisible on the null cone. Gravity theorists deriving Einstein-shaped balance from all-null Clausius data would cite it. Argument is finite-dimensional linear algebra over the Minkowski null cone, built on the Clausius–Einstein bridge.

claimFor symmetric matrix sources $S$, the quadratic null contraction $q(k)=k^{\mathsf T}Sk$ (Minkowski-null $k$) is additive and homogeneous; $q$ vanishes on pure metric terms $S\propto g$; an Einstein-shaped source yields a null scalar fixed by the matter side; the RS null-field reduction certificate packages that the residual freedom is only a scalar multiple of the metric.

background

Recognition Science gravity work routes local thermodynamic balance into field equations through Jacobson's Clausius argument. The imported bridge module isolates the finite-dimensional hinge: equality of two symmetric quadratic forms on every Minkowski-null direction fixes their difference only up to a scalar multiple of the metric, so an all-null Clausius balance already has the algebraic shape of Einstein's equation with the metric term free.

This module works at the matrix level. Quadratic contraction $q_S(k)=k^{\mathsf T}Sk$ is the observable along null vectors. Einstein-shaped sources are those whose null contractions match a prescribed matter scalar. Constants supplies the RS-native tick scale used elsewhere in the gravity stack; the local algebra here is dimensionless linear algebra on symmetric matrices.

Sibling lemmas establish additivity and homogeneity of $q$, vanishing of $q$ on pure $g$-terms ("null-invisible" metric pieces), reconstruction of sources from componentwise data, and the packaged reduction certificate.

proof idea

Not a single theorem: a short lemma stack. Additivity and scalar-homogeneity of quadratic contraction are direct expansions. The metric-term lemma shows $k^{\mathsf T}gk=0$ on the Minkowski null cone, so pure cosmological-constant-like pieces drop out of all-null balance. Einstein-shaped and RS-null-scalar constructors identify the null scalar read off a source; componentwise source assembly feeds those constructors. The reduction certificate aggregates the null-invisibility and shape facts into one audit-facing Prop/witness pair for downstream checking.

why it matters in Recognition Science

Closes the algebraic step from all-null local balance to an Einstein-shaped field equation inside the RS gravity path, leaving only the undetermined metric multiple that standard GR also leaves to separate normalization. Feeds RSNullFieldEquationAudit, whose doc-comment states it is the axiom audit for this matrix-level RS null-field reduction. Sits downstream of the Clausius–Einstein bridge and upstream of any continuum or curvature identification that must justify ignoring pure-$g$ residuals on the null cone. Landmark contact is thermodynamic gravity (Jacobson-style), not the T0–T8 forcing chain directly.

scope and limits

used by (1)

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 (11)