Gravity Null Cone Quadratic Tensor Class Symmetric Null Zero Eq Scalar Eta Compo

Null-cone rigidity

In the four-dimensional spacetime of special relativity, a covector is a linear map from vectors to numbers. A covector is called null when its squared length, computed with the Minkowski metric η = diag(-1,1,1,1), is zero; these are the directions along which light travels. A symmetric quadratic form, built from a 4 by 4 symmetric matrix D by contracting it with a covector k to get kᵀDk, assigns a number to every covector. The theorem at issue asks what it means for such a form to vanish on every null covector.

The answer is a rigidity statement. If a symmetric matrix D gives zero when contracted with every null covector, then D must itself be a scalar multiple of the Minkowski metric: there exists a real number λ such that D = λη, meaning Dᵢⱼ = ληᵢⱼ for every pair of indices i and j. This is the content of the declaration symmetric_null_zero_eq_scalar_eta_components, a theorem in the framework's machine-checked library of formal theorems. The proof is short: the hypothesis says D agrees with the zero matrix on the null cone, and the general reconstruction theorem then forces the difference, which is D itself, to be a scalar multiple of η.

The result is a purely algebraic fact about real 4 by 4 matrices. It does not identify D with any physical tensor such as the Ricci curvature or the stress-energy tensor. It does not construct horizons, derive a temperature, or close the Einstein field equation. The theorem is a prerequisite, not a physical conclusion: it says that if a symmetric object of this shape vanishes on lightlike directions, its only freedom is an overall scale set by the metric. The antisymmetric part of any matrix is invisible to this contraction, which is why the statement requires symmetry as a hypothesis.

In Recognition Science, this rigidity result is a step toward a larger goal. The framework aims to derive gravitational structure from a ledger of recognition events, and this theorem is an algebraic tool for that program. It is tagged THEOREM in the library, meaning it is proved with no unproved assumptions beyond the standard axioms of the ambient type theory. What remains open is the construction of a symmetric tensor G with a genuine Recognition ancestry, independent of any fixed stress tensor. This theorem does not supply that G; it only constrains what such a G could look like if it vanishes on the null cone.

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

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

This theorem does not identify D with the Ricci curvature or the stress-energy tensor. This theorem does not construct horizons, derive a temperature, or close the Einstein field equation. This theorem does not provide the independently geometric tensor G required for Phase 5.

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: