Gravity Rsnull Field Equation Null Scalar Of Einstein Shaped

The null scalar reduction

Einstein's field equations relate the curvature of spacetime, encoded in the Ricci tensor, to the distribution of matter and energy, encoded in the stress-energy tensor. The full equation is a matrix equation: it holds for every pair of spacetime directions at once. But there is a special class of directions, called null or lightlike, along which light itself travels. Probing the equation along such a direction simplifies it dramatically.

The Recognition Science library, a machine-checked collection of formal theorems, proves this simplification in a precise algebraic setting. The theorem, named null_scalar_of_einstein_shaped, starts from an assumption: that a matrix equation of the form κ T = Ric + f η holds, where κ is a coupling constant, T is the stress-energy tensor, Ric is the Ricci tensor, f is an unknown scalar function, and η is the Minkowski metric. When you contract this equation twice with a null vector k, meaning you evaluate it along a lightlike direction, the metric term f η vanishes because η(k,k) = 0 by definition of null. What remains is the scalar equation Ric(k,k) = κ T(k,k).

This is a purely algebraic result. It does not construct a solution to Einstein's equations, nor does it derive the field equations from first principles. The theorem takes the Einstein-shaped matrix equation as an input, supplied from outside the framework, and shows what its null contraction must be. The library also proves a companion fact: the scalar metric term f is invisible to null contractions. Adding any multiple of η to the Ricci tensor changes the matrix but leaves every null contraction unchanged, so the null scalar equation alone cannot recover that term.

In Recognition Science, this reduction is a stepping stone. The framework's own coupling constant κ is selected as kappa_einstein, and the theorem rs_null_scalar_of_source bundles the result with that choice. But the physical bridge, connecting the framework's ledger of recognition events to a sourced field equation, remains open. What this theorem establishes is a clean algebraic fact: along null directions, the Einstein-shaped equation reduces to a scalar relation, and the undetermined metric term drops out.

/--
Null reduction of one Einstein-shaped equation.  The undetermined scalar
metric term disappears on every Minkowski-null direction.
-/
theorem null_scalar_of_einstein_shaped
    (coupling : ℝ)
    (T Ric : Matrix (Fin 4) (Fin 4) ℝ)
    (f : ℝ)
    (h : coupling • T = Ric + f • minkowskiEta4)
    (k : Fin 4 → ℝ)
    (hk : MinkowskiNull k) :
    quadContr Ric k = coupling * quadContr T k := by
  have hcontract := congrArg (fun A => quadContr A k) h
  change quadContr (coupling • T) k =
    quadContr (Ric + f • minkowskiEta4) k at hcontract
  rw [quadContr_smul, quadContr_add,
    quadContr_metric_term_eq_zero f k hk, add_zero] at hcontract
  exact hcontract.symm

/-- Every scalar Minkowski metric term vanishes on a null probe. -/
theorem quadContr_metric_term_eq_zero
    (f : ℝ) (k : Fin 4 → ℝ)
    (hk : MinkowskiNull k) :
    quadContr (f • minkowskiEta4) k = 0 := by
  rw [quadContr_smul, quadContr_minkowskiEta4]
  rw [show -(k 0) ^ 2 + (k 1) ^ 2 + (k 2) ^ 2 + (k 3) ^ 2 = 0 by
    simpa [MinkowskiNull] using hk]
  ring

/--
The null equation does not recover the scalar metric term: adding a nonzero
multiple of `η` changes the matrix while preserving every null contraction.
-/
theorem scalar_metric_term_is_null_invisible :
    ∃ D : Matrix (Fin 4) (Fin 4) ℝ,
      D ≠ 0 ∧
      ∀ k, MinkowskiNull k → quadContr D k = 0 := by
  refine ⟨minkowskiEta4, ?_, ?_⟩
  · intro h
    have h00 := congrFun (congrFun h (0 : Fin 4)) (0 : Fin 4)
    norm_num [minkowskiEta4] at h00
  · intro k hk
    simpa using quadContr_metric_term_eq_zero 1 k hk

/--
An Einstein-shaped sourced equation at the matrix layer.  This is an explicit
input interface, not an in-tree derivation from the RS action.
-/
def EinsteinShapedSource
    (coupling : ℝ)
    (T Ric : Matrix (Fin 4) (Fin 4) ℝ) : Prop :=
  ∃ f : ℝ, coupling • T = Ric + f • minkowskiEta4

What this page does not claim

This theorem does not construct a horizon patch or identify cut channels with spacetime covectors. It does not derive a sourced field equation from the ledger; the source is assumed, not derived. The null scalar equation does not recover the undetermined scalar metric term f.

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/RSNullFieldEquation.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: