Gravity Analysis Edge Ttdecomposition Lorentz4 D Lorentz Load Transverse Project

The transverse projector

In general relativity, gravitational waves are transverse and traceless: they wiggle perpendicular to their direction of travel and leave volumes unchanged. The declaration lorentzLoad_transverseProjector is a piece of linear algebra, not physics itself. It takes a symmetric 4 by 4 matrix, which stands for a small disturbance in the spacetime metric, and a wave covector, which stands for the direction the wave travels, and produces a new matrix that is transverse to that direction. Transverse here means that contracting the matrix's second index against the raised wave covector gives zero for every row, a condition written as a set of four equations.

The construction uses the Minkowski metric with signature (-,+,+,+), the standard convention where time enters with a minus sign. The projector is defined as the metric minus a rank-one term built from the wave covector, scaled by the inverse of its Minkowski norm squared: P = η - m mᵀ / (m·m). This formula works when the wave covector is non-null, meaning its Minkowski norm squared is not zero. The declaration also covers the physically important null case, where the wave travels at the speed of light and the norm squared is zero. There the projector needs an auxiliary null covector l and takes the form P = η - (m lᵀ + l mᵀ) / (m·l).

The broader file this belongs to, the edge TT decomposition in four dimensions, proves that this projection, together with a trace removal step, splits any symmetric matrix into a transverse-traceless part, a gauge part, and a trace part. The theorems in the file are machine-checked: they are verified in a formal library of theorems with no unproved assumptions beyond the standard logical axioms. The declaration itself is a definition, not a theorem; the theorems around it establish that the projected matrix is symmetric, transverse, and traceless when the input is symmetric.

What this does not claim is just as important. It does not decompose actual perturbations on a lattice of spacetime edges, which would be a discrete gravity calculation. It does not prove that the Recognition Science action converges to the Einstein-Hilbert action in four dimensions. It attaches no physical normalization to the polarization of gravitational waves. The declaration is a clean algebraic tool: it isolates the transverse part of a metric disturbance in a way that respects the Lorentzian signature, and the framework's library checks that the algebra is correct.

def transverseProjector (m : Fin 4 → ℝ) : Mat4 :=
  minkowskiEta - (minkowskiDot m m)⁻¹ • outerSq m

def transverseProjector (m : Fin 4 → ℝ) : Mat4 :=
  minkowskiEta - (minkowskiDot m m)⁻¹ • outerSq m

theorem nullPhp_symmetric (m l : Fin 4 → ℝ) (H : Mat4)
    (hH : IsSymmetric H) :
    IsSymmetric (nullPhp m l H) := by
  intro i j
  unfold nullPhp
  calc
    ∑ a : Fin 4, ∑ b : Fin 4,
        nullPMixed m l i a * H a b * nullPMixed m l j b
        = ∑ b : Fin 4, ∑ a : Fin 4,
            nullPMixed m l i a * H a b * nullPMixed m l j b := by
      rw [Finset.sum_comm]
    _ = ∑ b : Fin 4, ∑ a : Fin 4,
            nullPMixed m l j b * H b a * nullPMixed m l i a := by
      refine Finset.sum_congr rfl fun b _ => Finset.sum_congr rfl fun a _ => ?_
      rw [hH a b]; ring
    _ = ∑ a : Fin 4, ∑ b : Fin 4,
        nullPMixed m l j a * H a b * nullPMixed m l i b := by
      rw [Finset.sum_comm]

What this page does not claim

It does not decompose actual perturbations on a lattice of spacetime edges. It does not prove that the Recognition Science action converges to the Einstein-Hilbert action in four dimensions. It attaches no physical normalization to the polarization of gravitational waves.

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/Analysis/EdgeTTDecompositionLorentz4D.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: