Gravity Rsnull Field Equation Quad Contr Smul

The contraction rule

In the Recognition Science framework, recognition (a discrete record of events) is used to build a matrix equation shaped like Einstein's field equation. The declaration quadContr_smul establishes a basic algebraic property of the quadratic contraction operation used to reduce that matrix equation along a null direction, a direction in spacetime along which light travels. The property is homogeneity: multiplying the matrix by a scalar factor before contracting is the same as contracting first and then multiplying the result by that same scalar. In symbols, for any real number c, any 4x4 matrix A, and any null vector k, quadContr (c • A) k = c * quadContr A k.

This rule is a theorem in the framework's machine-checked library of formal theorems. It is the second of two linearity properties, the first being additivity: quadContr (A + B) k = quadContr A k + quadContr B k. Together they mean the contraction is a linear operation on the matrix argument. The homogeneity rule is what allows the framework to pull the coupling constant out of the contraction, a step that appears in the reduction of an Einstein-shaped source equation to its null-contracted scalar form. That reduction is the framework's bridge from a matrix-level field equation to a scalar equation along a null probe.

The declaration does not claim that the matrix equation itself is derived from the ledger of recognition events. The framework explicitly marks the existence of an EinsteinShapedSource as an external input, not an in-tree derivation. The homogeneity rule also does not claim that the null contraction can recover the full matrix equation. A separate theorem in the same module shows that a nonzero multiple of the Minkowski metric is invisible to every null contraction: adding it to a matrix changes the matrix but leaves all null contractions unchanged. The scalar metric term is therefore not recoverable from null data alone.

What the rule does is make the algebra of null reduction precise and checkable. It is a small but load-bearing step in the framework's program of forcing physical structure from recognition. The payoff is not a new physical prediction but a verified piece of the formal chain: when a null direction probes an Einstein-shaped source with the framework's coupling, the metric term vanishes and the scalar equation Ric(k,k) = κ T(k,k) follows. The homogeneity rule is what lets the coupling constant κ pass cleanly through the contraction, so the reduction is exact and not an approximation.

/-- Quadratic contraction is homogeneous in its matrix argument. -/
theorem quadContr_smul
    (c : ℝ) (A : Matrix (Fin 4) (Fin 4) ℝ)
    (k : Fin 4 → ℝ) :
    quadContr (c • A) k = c * quadContr A k := by
  unfold quadContr
  simp only [Matrix.smul_apply, smul_eq_mul]
  calc
    (∑ i, ∑ j, c * A i j * k i * k j)
        = ∑ i, ∑ j, c * (A i j * k i * k j) := by
          refine Finset.sum_congr rfl fun i _ =>
            Finset.sum_congr rfl fun j _ => by ring
    _ = ∑ i, c * ∑ j, A i j * k i * k j := by
          refine Finset.sum_congr rfl fun i _ =>
            (Finset.mul_sum _ _ _).symm
    _ = c * ∑ i, ∑ j, A i j * k i * k j :=
      (Finset.mul_sum _ _ _).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

What this page does not claim

The declaration does not derive the Einstein-shaped source equation from the ledger; that source is an explicit external input. The declaration does not claim that null contractions can recover the full matrix equation, since a nonzero metric term is invisible to them. The declaration does not construct a horizon patch or identify cut channels with spacetime covectors.

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: