Pith. sign in
module module moderate

IndisputableMonolith.Gravity.NullConeQuadraticTensorClass

show as:
view Lean formalization →

Finite-dimensional linear algebra for quadratic forms on the Minkowski null cone in 3+1 dimensions. The module defines componentwise symmetrization of real 4×4 matrices, quadratic contractions, and proves that null-cone values see only the symmetric part, with the antisymmetric part vanishing. Gravity workers reconstructing Jacobson's Clausius-to-Einstein hinge cite these lemmas. Arguments are direct index algebra and Fin-4 summations.

claimFor a real $4\times 4$ matrix $T$, let $\mathrm{Sym}(T)$ be its componentwise symmetrization and $Q_T(v)=T_{\mu\nu}v^\mu v^\nu$ its quadratic contraction. Then $Q_T=Q_{\mathrm{Sym}(T)}$ on all vectors, the antisymmetric part has $Q=0$, and if $Q_A=Q_B$ on every future nonzero Minkowski-null vector then $Q_{A-B}=0$ on the full null cone. Scalar multiples of the metric $\eta$ contribute only through the null condition $v\cdot v=0$.

background

Jacobson's thermodynamic route to the Einstein equation reduces, at the algebraic hinge, to a statement about quadratic forms on null directions: if two symmetric bilinear forms agree on every Minkowski-null vector, their difference is a scalar multiple of the metric. The upstream module ClausiusEinsteinBridge isolates that hinge: "Equality of two symmetric quadratic forms on every Minkowski-null direction determines their difference only up to a scalar multiple of the metric."

This module supplies the supporting 4×4 tensor calculus. It introduces componentwise symmetrization and antisymmetrization of real matrices indexed by Fin 4, the quadratic contraction $Q_T(v)$, and elementary identities for scaling by scalars and by the Minkowski metric $\eta$. The ambient setting is flat 3+1 signature; no curvature or field equations appear yet.

Notation is componentwise: symmetrize averages $T_{\mu\nu}$ with $T_{\nu\mu}$; the null cone is ${v:v\cdot v=0}$, with a future-nonzero restriction used to extend identities to the full cone.

proof idea

The module is a short library of algebraic lemmas, not a single theorem. Symmetrization is defined componentwise; symmetry of the result and the projector identity on already-symmetric matrices are immediate. Quadratic contraction is shown invariant under symmetrization by expanding the bilinear form and cancelling cross terms. The antisymmetric part contracts to zero against any $v\otimes v$ by the same expansion. Negation and scalar-multiplication rules for $Q_T$ are one-line. Agreement on future nonzero null vectors is extended to the full null cone by a sign/scaling argument. Contractions against multiples of $\eta$ reduce via $v\cdot v=0$ on the null cone.

why it matters in Recognition Science

Phase-5 of the gravity stack needs a clean algebraic null-cone rigidity prerequisite before the Clausius balance can be rewritten as Einstein's equation with an undetermined cosmological term. This module packages that prerequisite: symmetrization, vanishing of the antisymmetric contribution, and null-cone extension lemmas that the bridge theorem consumes.

It is imported by NullConeQuadraticTensorClassAudit, whose doc-comment calls it the "Axiom audit for the Phase-5 algebraic null-cone rigidity prerequisite." Downstream audit and bridge modules therefore treat these identities as the trusted linear-algebra layer rather than re-proving index identities in situ.

Within Recognition Science gravity, the result is infrastructure for the thermodynamic derivation path, not a claim about dynamics, horizons, or the RS forcing chain (T0–T8). It keeps the metric-ray freedom explicit, matching the upstream hinge statement that the metric term is left free.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (27)