Gravity Null Cone Quadratic Tensor Class All Null Quad Eq Of Future Nonzero Null

The null cone's verdict

In the geometry of spacetime, the null cone is the set of directions along which light travels: vectors whose squared length, measured with the Minkowski metric of signature (-1,1,1,1), is exactly zero. A symmetric 4x4 matrix, like the stress-energy tensor of general relativity, assigns a number to each such direction by contracting the matrix with the vector twice. The question is how much information those numbers carry.

The theorem all_null_quad_eq_of_future_nonzero_null_quad_eq answers a sharp version of that question. It says: if two symmetric matrices agree on all future-pointing, nonzero null directions, then they agree on all null directions, including past-pointing and zero ones. The proof is short: a past-pointing null vector is the negative of a future-pointing one, and the quadratic form is unchanged by that sign flip. The zero vector is handled by direct computation. This is a pure algebraic fact about real 4x4 matrices, proved in the framework's machine-checked library of formal theorems.

The deeper result this supports is a reconstruction theorem. If two symmetric matrices agree on the entire null cone, they are not necessarily equal; they can differ by any scalar multiple of the Minkowski metric itself. That metric vanishes on every null vector, so such a difference is invisible to the quadratic form. The theorem proves the converse too: any two symmetric matrices that agree on the null cone differ by exactly such a scalar multiple. Together these statements mean the null cone's values determine the matrix up to a single real number.

This rigidity is a prerequisite for a later phase of the framework's program, one that aims to construct a geometric tensor from recognition area and focusing data. The theorem itself does not do that construction. It does not identify any matrix with the Ricci tensor or stress-energy, does not build horizons or Unruh temperature, and does not close the Einstein field equation. Those remain open targets. What the theorem establishes is narrower but firm: the null cone's verdict on a symmetric matrix is nearly complete, leaving exactly one scalar degree of freedom free.

/--
Agreement on every future nonzero Minkowski-null vector extends to the whole
null cone.  Negative-time vectors are handled by quadratic evenness.  A null
vector with zero time component is the zero vector.
-/
theorem all_null_quad_eq_of_future_nonzero_null_quad_eq
    (A B : Matrix (Fin 4) (Fin 4) ℝ)
    (hfuture :
      ∀ k, MinkowskiNull k → k ≠ 0 → 0 < k 0 →
        quadContr A k = quadContr B k) :
    ∀ k, MinkowskiNull k → quadContr A k = quadContr B k := by
  intro k hk
  by_cases hzero : k = 0
  · subst k
    simp [quadContr]
  have htime : k 0 ≠ 0 := by
    intro hk0
    have hkEq := hk
    unfold MinkowskiNull at hkEq
    norm_num [hk0] at hkEq
    have h1 : k 1 = 0 := by
      nlinarith [sq_nonneg (k 1), sq_nonneg (k 2), sq_nonneg (k 3)]
    have h2 : k 2 = 0 := by
      nlinarith [sq_nonneg (k 1), sq_nonneg (k 2), sq_nonneg (k 3)]
    have h3 : k 3 = 0 := by
      nlinarith [sq_nonneg (k 1), sq_nonneg (k 2), sq_nonneg (k 3)]
    apply hzero
    funext i
    fin_cases i
    · exact hk0
    · exact h1
    · exact h2
    · exact h3
  rcases lt_or_gt_of_ne htime with hneg | hpos
  · have hkneg : MinkowskiNull (-k) := by
      simpa [MinkowskiNull] using hk
    have hnegzero : (-k) ≠ 0 := neg_ne_zero.mpr hzero
    have hfutureNeg :=
      hfuture (-k) hkneg hnegzero (by simpa using neg_pos.mpr hneg)
    simpa only [quadContr_neg] using hfutureNeg
  · exact hfuture k hk hzero hpos

/-- Quadratic contraction is even in its vector argument. -/
theorem quadContr_neg
    (A : Matrix (Fin 4) (Fin 4) ℝ) (k : Fin 4 → ℝ) :
    quadContr A (-k) = quadContr A k := by
  unfold quadContr
  refine Finset.sum_congr rfl fun i _ => ?_
  refine Finset.sum_congr rfl fun j _ => ?_
  simp only [Pi.neg_apply]
  ring

/-- Biconditional for symmetric matrices. -/
theorem null_quadratic_eq_iff_diff_scalar_eta
    (A B : Matrix (Fin 4) (Fin 4) ℝ)
    (hA : Symmetric4 A)
    (hB : Symmetric4 B) :
    (∀ k, MinkowskiNull k → quadContr A k = quadContr B k) ↔
      ∃ lam : ℝ, ∀ i j, A i j - B i j = lam * minkowskiEta4 i j := by
  constructor
  · exact null_quadratic_eq_implies_diff_scalar_eta A B hA hB
  · intro h
    obtain ⟨lam, hlam⟩ := h
    exact diff_scalar_eta_implies_null_quadratic_eq A B lam hlam

What this page does not claim

The theorem does not construct any geometric tensor. The theorem does not identify any matrix with the Ricci tensor or stress-energy. The theorem does not build horizons or Unruh temperature.

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: