Gravity Rsnull Field Equation Rs Null Scalar Of Source

The null scalar reduction

In the Recognition Science framework, recognition (a discrete record of events) is used to build physical structure. The declaration rs_null_scalar_of_source is a theorem in the framework's machine-checked library of formal theorems. It proves a specific algebraic step: if you start with a matrix equation shaped like the Einstein field equation, and you contract it with a Minkowski-null vector, then the metric term vanishes and you are left with a scalar equation relating the Ricci curvature to the source.

The theorem is stated in the language of 4x4 real matrices. It assumes an EinsteinShapedSource, which is an input interface: a matrix equation of the form κT = Ric + fη, where κ is a coupling constant, T is the stress-energy source, Ric is the Ricci curvature matrix, f is an undetermined scalar, and η is the Minkowski metric. The declaration proves that for any Minkowski-null vector k (meaning k satisfies η(k,k) = 0), the contraction of the Ricci matrix with k equals κ times the contraction of the source matrix with k. In symbols, Ric(k,k) = κ T(k,k).

The proof follows from two lemmas: the quadratic contraction is linear in its matrix argument, and the scalar metric term vanishes on a null probe. The framework's specialization selects the coupling parameter κ = kappa_einstein. The theorem is tagged THEOREM in the library, meaning all the matrix and null-contraction algebra is formally verified.

What this theorem does not claim is as important as what it proves. The declaration does not construct a horizon patch, does not identify cut channels with spacetime covectors, and does not derive a sourced field equation from the ledger. Inhabiting the EinsteinShapedSource from the RS action is an open problem, not a theorem. The file name is retained for import compatibility, but every public declaration is named as a conditional reduction rather than a derived field equation.

The practical upshot is a clean, verified bridge from a matrix equation to a scalar one, with the metric term shown to be invisible to null contractions. This is a useful tool for anyone working with null geodesics or gravitational wave propagation within the framework. It is not, however, a derivation of the field equation itself, and it does not recover the undetermined scalar f from the null data.

/--
RS-normalized specialization: an independently inhabited Einstein-shaped
source with the RS coupling yields its null-contracted scalar form.
-/
theorem rs_null_scalar_of_source
    {T Ric : Matrix (Fin 4) (Fin 4) ℝ}
    (h : EinsteinShapedSource kappa_einstein T Ric) :
    ∀ k, MinkowskiNull k →
      quadContr Ric k = kappa_einstein * quadContr T k :=
  null_scalar_of_source h

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

What this page does not claim

The theorem does not construct a horizon patch. The theorem does not identify cut channels with spacetime covectors. The theorem does not derive a sourced field equation from the ledger.

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: