Gravity Null Cone Quadratic Tensor Class Determines Algebraic Null Quadratic Cla

The reconstruction theorem

In four-dimensional spacetime, a symmetric matrix can be thought of as a machine that assigns a real number to each direction. The direction is a four-vector, and the number is the quadratic form evaluated on it. A lightlike direction, also called a null direction, is one for which the Minkowski metric gives zero: for a vector (t, x, y, z), this means t² = x² + y² + z². The Minkowski metric η = diag(-1,1,1,1) is the standard spacetime interval.

The result in question, determinesAlgebraicNullQuadraticClass_quadContr, proves a rigidity property. One can know the values of a symmetric quadratic form on every null direction. The result says this information determines the entire matrix, except for one ambiguity: you cannot distinguish a matrix A from A + λη, where λ is any real number, because η evaluates to zero on every null direction. This is the precise sense in which the null cone pins down the quadratic form.

The result is part of a larger algebraic package. Its proof rests on a key lemma: if two symmetric matrices agree on all null directions, their difference must be a scalar multiple of η. The converse also holds. The package also shows that the antisymmetric part of any matrix is invisible to this construction, and that symmetrization is the only operation that matters for null-cone values. These results are proved in the machine-checked library of formal theorems, with no unproved assumptions.

In Recognition Science, this result is a prerequisite for a later phase of work on gravity. It is not itself a statement about physics. It does not identify any matrix with the Ricci tensor or the stress-energy tensor. It does not construct horizons or derive the Einstein field equation. Those remain open targets. The result is purely algebraic: it says what can and cannot be learned about a symmetric matrix from its null-cone values.

The practical consequence is a clean classification. Any symmetric matrix belongs to a class determined by its null-cone values, and two matrices in the same class differ only by a multiple of the metric. This is exactly the ambiguity one expects from the light cone, and the result makes it precise. It is a tool, not a physical law, and its limits are as sharp as its statement.

/--
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

/-- 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

/-- 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

What this page does not claim

The theorem does not construct a geometric tensor with Recognition area ancestry. The theorem does not close the Einstein field equation. The theorem does not identify the matrix with Ricci or stress-energy.

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: