Gravity Null Cone Quadratic Tensor Class Fixed Symmetric Stress Determines Algeb

Reading a fixed stress tensor

In four-dimensional spacetime, a symmetric matrix T with entries T_ij = T_ji describes a stress-energy distribution. The declaration in question, fixedSymmetricStress_determinesAlgebraicNullQuadraticClass, states a precise rigidity fact: if you know the value of the quadratic form k ↦ k^TTk for every lightlike (null) covector k, then you know T itself, up to adding a scalar multiple of the Minkowski metric η = diag(-1,1,1,1). In symbols, if two symmetric matrices T and B give the same values on all null k, then T - B = λη for some real number λ. This is a theorem in the framework's machine-checked library of formal theorems.

The content is purely algebraic and finite-dimensional. It does not identify T with Ricci curvature or stress-energy of any particular physical field. It does not construct horizons, derive Unruh temperature, or close the Einstein field equation. The theorem is a prerequisite for a later phase of the framework's gravity program, not a physical law by itself. The framework's own documentation marks the construction of an independent geometric tensor from Recognition area/focusing ancestry as OPEN; this declaration only establishes the algebraic uniqueness of a fixed stress tensor's null-cone values.

The proof rests on a chain of lemmas in the same module. One key step shows that the antisymmetric part of any matrix is invisible to the null-cone quadratic form: quadContr A k = quadContr (symmetrize4 A) k for all k. Another shows that if two symmetric matrices agree on all null directions, their difference is a scalar multiple of η. The theorem also has a converse: if two matrices differ by a scalar multiple of η, they agree on all null directions. Together these give a complete characterization of the equivalence class of matrices that produce the same null-cone values.

In Recognition Science, this result is a building block for a larger project of deriving gravity from recognition events. The framework models spacetime structure through such algebraic rigidity facts, and this one says that a fixed symmetric stress tensor's information content is exactly its null-cone quadratic values, up to the single η-ambiguity. That ambiguity is physically meaningful: it corresponds to the freedom to add a cosmological-constant-like term without changing lightlike physics. The theorem does not, however, say that any particular stress tensor is physically realized or that the Einstein equations hold.

/--
Null-cone agreement of two symmetric quadratic forms determines their
difference as a scalar multiple of the Minkowski metric.
-/
theorem null_quadratic_eq_implies_diff_scalar_eta
    (A B : Matrix (Fin 4) (Fin 4) ℝ)
    (hA : Symmetric4 A)
    (hB : Symmetric4 B)
    (hnull : ∀ k, MinkowskiNull k → quadContr A k = quadContr B k) :
    ∃ lam : ℝ, ∀ i j, A i j - B i j = lam * minkowskiEta4 i j := by
  obtain ⟨lam, hlam⟩ := null_quadratic_eq_of_diff_scalar_eta A B hA hB hnull
  refine ⟨lam, ?_⟩
  intro i j
  have hij := congrFun (congrFun hlam i) j
  -- `A = B + lam • η` at `(i,j)`.
  change A i j = B i j + (lam • minkowskiEta4) i j at hij
  simp only [Matrix.smul_apply, smul_eq_mul] at hij
  linarith

/-- Quadratic contraction sees only the symmetric part. -/
theorem quadContr_eq_quadContr_symmetrize4
    (A : Matrix (Fin 4) (Fin 4) ℝ) (k : Fin 4 → ℝ) :
    quadContr A k = quadContr (symmetrize4 A) k := by
  simp only [quadContr, symmetrize4, sum_fin_four]
  ring

/-- Converse: a pure metric difference is invisible on the null cone. -/
theorem diff_scalar_eta_implies_null_quadratic_eq
    (A B : Matrix (Fin 4) (Fin 4) ℝ) (lam : ℝ)
    (hlam : ∀ i j, A i j - B i j = lam * minkowskiEta4 i j) :
    ∀ k, MinkowskiNull k → quadContr A k = quadContr B k := by
  intro k hk
  have hAB : A = B + lam • minkowskiEta4 := by
    ext i j
    have hij := hlam i j
    simp only [Matrix.add_apply, Matrix.smul_apply, smul_eq_mul]
    linarith
  have hcontr := congrArg (fun M => quadContr M k) hAB
  change quadContr A k = quadContr (B + lam • minkowskiEta4) k at hcontr
  have hadd :
      quadContr (B + lam • minkowskiEta4) k =
        quadContr B k + quadContr (lam • minkowskiEta4) k := by
    simp only [quadContr, Matrix.add_apply, add_mul, Finset.sum_add_distrib]
  rw [hadd, quadContr_smul_eta_of_null lam k hk, add_zero] at hcontr
  exact hcontr

What this page does not claim

The theorem does not identify any matrix with Ricci curvature or stress-energy of a specific field. It does not construct horizons, derive Unruh temperature, or close the Einstein field equation. It does not say that any particular stress tensor is physically realized.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/NullConeQuadraticTensorClass.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: