Pith. sign in
module module high

IndisputableMonolith.Gravity.NullConeQuadraticTensorClass

show as:
view Lean formalization →

Algebraic toolkit for real 4×4 tensors acting as quadratic forms on Minkowski null vectors. It isolates componentwise symmetrization, antisymmetrization, and null-cone quadratic contractions, proving that only the symmetric part contributes on null directions. Gravity and thermodynamics workers cite it when reducing an all-null Clausius balance to Einstein shape. Arguments are finite-dimensional linear algebra identities on Fin 4 indices.

claimFor real $4\times 4$ tensors $T$, define the componentwise symmetrization $\mathrm{Sym}(T)_{\mu\nu}=\frac12(T_{\mu\nu}+T_{\nu\mu})$ and the quadratic contraction $Q_T(v)=T_{\mu\nu}v^\mu v^\nu$. On Minkowski-null $v$ one has $Q_T(v)=Q_{\mathrm{Sym}(T)}(v)$, the antisymmetric part contributes zero, and scaling by the metric $\eta$ acts by a pure scalar on the null cone.

background

Recognition Science gravity work follows Jacobson's thermodynamic route: a local Clausius balance on every null generator should force Einstein's equation up to a free cosmological term. The upstream module ClausiusEinsteinBridge isolates the finite-dimensional hinge: "Equality of two symmetric quadratic forms on every Minkowski-null direction determines their difference only up to a scalar multiple of the metric."

Before that rigidity statement can be stated cleanly, one needs a small tensor calculus layer. This module supplies it. Objects are real maps on $\mathrm{Fin},4\times\mathrm{Fin},4$; symmetrize4 and antisymmetrize4 split any tensor into symmetric and skew parts; quadContr is the associated quadratic form $v\mapsto T_{\mu\nu}v^\mu v^\nu$. The null cone is the set of nonzero future (or all) vectors with $\eta(v,v)=0$.

Sibling lemmas record elementary identities: quadratic contraction ignores the antisymmetric part, is homogeneous under scalar multiples, and for multiples of $\eta$ collapses on null vectors to zero (or a controlled scalar off-null).

proof idea

Definition-heavy module with short algebraic proofs, not a single top-level theorem. symmetrize4 is the component average; symmetrize4_symmetric and symmetrize4_of_symmetric are immediate unfolding. antisymmetrize4 is the skew counterpart. quadContr_eq_quadContr_symmetrize4 expands the bilinear form and cancels cross terms by commutativity of multiplication in $\mathbb{R}$. quadContr_antisymmetrize4_eq_zero is the same cancellation for the skew part. Homogeneity lemmas (quadContr_smul, quadContr_smul_eta, quadContr_smul_eta_of_null) are one- or two-line rewrites. all_null_quad_eq_of_future_nonzero_null_quad_eq extends an identity from future null vectors to the full null cone by sign flip and density of the future sheet.

why it matters in Recognition Science

This is the Phase-5 algebraic prerequisite for null-cone rigidity in the RS gravity stack. Downstream, NullConeQuadraticTensorClassAudit imports the module as an "Axiom audit for the Phase-5 algebraic null-cone rigidity prerequisite," checking that no hidden axioms leak into the tensor identities.

The parent scientific claim lives in ClausiusEinsteinBridge: once two symmetric quadratic forms agree on every null direction, their difference is a multiple of the metric, which is exactly the algebraic shape of Einstein's equation with free cosmological constant. Without a verified symmetrization and null-contraction layer, that hinge cannot be stated in Lean.

In the broader Recognition framework the module is infrastructure rather than a forcing-chain step (T0–T8). It supports the thermodynamic derivation of Einstein gravity that RS uses when matching continuum GR to the discrete recognition ledger, keeping the metric term free exactly as Jacobson's argument requires.

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)