Encyclopedia Gravity Gravity Null Cone Quadratic Tensor Class Future Null Quadratic Eq Implies Diff S

ARTICLE 4 claims 4 theorems

Gravity Null Cone Quadratic Tensor Class Future Null Quadratic Eq Implies Diff S

A theorem about 4x4 matrices says that knowing a symmetric matrix's values on lightlike vectors forces the result, up to one unavoidable ambiguity.

Verify this page

Reading a quadratic form from its null cone

In special relativity, the Minkowski metric η = diag(-1,1,1,1) assigns a squared length to every four-vector. Vectors with zero squared length form the light cone, or null cone: the set of paths a flash of light could take. A symmetric 4x4 matrix A defines a quadratic form, a function that takes a vector k and returns the sum A[i][j] k[i] k[j]. The theorem future_null_quadratic_eq_implies_diff_scalar_eta asks a reconstruction question: if two symmetric matrices A and B produce identical values on every future-pointing null vector, what can differ between them?

The answer, proved in the framework's machine-checked library of formal theorems, is that A and B can differ only by a scalar multiple of the Minkowski metric itself. In symbols: if A and B are symmetric and quadContr A k = quadContr B k for every null k with positive time component, then there exists a real number λ such that A[i][j] - B[i][j] = λ η[i][j] for all indices i, j. The scalar λ is the single free parameter left undetermined by null-cone data. This is a rigidity result: the light cone carries almost all information about the matrix, except for one global rescaling direction.

The proof runs through a standard linear algebra argument. First, the theorem extends from future-pointing null vectors to all null vectors, because the quadratic form is even under k → -k. Then, a symmetric matrix D that vanishes on every null vector must itself be a scalar multiple of η. Subtracting the two matrices reduces the problem to that zero case. The library also records the converse: if two matrices differ by λη, they agree on all null vectors, since η itself vanishes on the null cone. Together these give an exact equivalence, not merely one direction.

In Recognition Science, this theorem is a Phase 5 algebraic prerequisite. It does not construct a geometric tensor, identify any matrix with Ricci curvature or stress-energy, or close the Einstein field equation. Those targets remain open. What the theorem supplies is a clean algebraic fact: the null-cone values of a symmetric quadratic form determine the form up to one scalar multiple of the metric. This is the kind of rigidity that later geometric steps would need, but the geometric steps themselves are not taken here.

THEOREM future_null_quadratic_eq_implies_diff_scalar_eta · IndisputableMonolith/Gravity/NullConeQuadraticTensorClass.lean
future_null_quadratic_eq_implies_diff_scalar_eta · IndisputableMonolith/Gravity/NullConeQuadraticTensorClass.lean:231 
/--
Future nonzero null agreement is sufficient for the symmetric rigidity
conclusion.  This is the algebraic handoff from future-section data; it does
not supply the independently constructed `G` required by Phase 5.
-/
theorem future_null_quadratic_eq_implies_diff_scalar_eta
    (A B : Matrix (Fin 4) (Fin 4) ℝ)
    (hA : Symmetric4 A)
    (hB : Symmetric4 B)
    (hfuture :
      ∀ k, MinkowskiNull k → k ≠ 0 → 0 < k 0 →
        quadContr A k = quadContr B k) :
    ∃ lam : ℝ, ∀ i j, A i j - B i j = lam * minkowskiEta4 i j := by
  apply null_quadratic_eq_implies_diff_scalar_eta A B hA hB
  exact all_null_quad_eq_of_future_nonzero_null_quad_eq A B hfuture
THEOREM all_null_quad_eq_of_future_nonzero_null_quad_eq · IndisputableMonolith/Gravity/NullConeQuadraticTensorClass.lean
all_null_quad_eq_of_future_nonzero_null_quad_eq · IndisputableMonolith/Gravity/NullConeQuadraticTensorClass.lean:120 
/--
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
THEOREM symmetric_null_zero_eq_scalar_eta_components · IndisputableMonolith/Gravity/NullConeQuadraticTensorClass.lean
symmetric_null_zero_eq_scalar_eta_components · IndisputableMonolith/Gravity/NullConeQuadraticTensorClass.lean:197 
/--
If a symmetric matrix has vanishing null-cone quadratic form, it is a scalar
multiple of `η`, stated componentwise.
-/
theorem symmetric_null_zero_eq_scalar_eta_components
    (D : Matrix (Fin 4) (Fin 4) ℝ)
    (hD : Symmetric4 D)
    (hnull : ∀ k, MinkowskiNull k → quadContr D k = 0) :
    ∃ lam : ℝ, ∀ i j, D i j = lam * minkowskiEta4 i j := by
  obtain ⟨lam, hlam⟩ := null_quadratic_zero_eq_scalar_eta D hD hnull
  refine ⟨lam, ?_⟩
  intro i j
  have hij := congrFun (congrFun hlam i) j
  simpa [Matrix.smul_apply, smul_eq_mul] using hij
THEOREM diff_scalar_eta_implies_null_quadratic_eq · IndisputableMonolith/Gravity/NullConeQuadraticTensorClass.lean
diff_scalar_eta_implies_null_quadratic_eq · IndisputableMonolith/Gravity/NullConeQuadraticTensorClass.lean:247 
/-- 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. The theorem does not construct horizons, Unruh temperature, or close the Einstein field equation. The theorem does not apply to antisymmetric matrices, whose null-cone values are identically zero.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND