Gravity Analysis Edge Ttdecomposition Lorentz4 D

The transverse-traceless split

The transverse-traceless (TT) decomposition is a standard tool in gravitational wave physics. It splits a symmetric 4x4 matrix, which represents a small disturbance of spacetime, into two pieces: one that describes the physical wave, and one that is a coordinate artifact, a gauge part. The wave piece is transverse, meaning it oscillates perpendicular to the direction of travel, and traceless, meaning its sum of diagonal entries vanishes. This split is what lets physicists count the two independent polarizations of a gravitational wave.

The module EdgeTTDecompositionLorentz4D in the framework's machine-checked library of formal theorems proves this decomposition for the full Lorentzian metric, with signature (-,+,+,+). The classical Euclidean version, where all four dimensions are treated alike, was already in the library. The new work handles the physically important case where the wave covector is null, meaning it points along a light ray. For a null wave, the usual projector formula divides by the squared length of the wave vector, which is zero, so the library constructs a different projector using an auxiliary null vector, and proves the split still works.

In Recognition Science, this is the Lorentzian linear-algebra layer of a larger campaign to connect the framework's discrete ledger of recognition events to Einstein's theory. The library proves that the TT decomposition holds for all symmetric matrices, for both non-null and null wave covectors, with no unproved axioms beyond the standard three. It does not itself decompose perturbations on a lattice, nor does it prove that the framework's action converges to the Einstein-Hilbert action in four dimensions. Those remain targets.

The practical payoff is that the framework now has a rigorous, machine-checked handle on the two physical degrees of freedom of a gravitational wave in four spacetime dimensions. When a later module needs to separate the wave from the gauge, this is the tool it will call. The proof is a theorem, not a model: it is a fact about 4x4 matrices with a Minkowski metric, checked line by line.

def ttProject (m : Fin 4 → ℝ) (H : Mat4) : Mat4 :=
  gaugeCorrected m H - residualTrace m H • transverseProjector m

def nullTTProject (m l : Fin 4 → ℝ) (H : Mat4) : Mat4 :=
  nullPhp m l H - nullTraceCoeff m l H • nullProjector m l

/-- Null-frame transverse projector against null `m` with auxiliary null `l`. -/
def nullProjector (m l : Fin 4 → ℝ) : Mat4 :=
  minkowskiEta - (minkowskiDot m l)⁻¹ • symmetrizedOuter m l

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

The module does not decompose perturbations on a 4D lattice. The module does not prove that the framework's action converges to the Einstein-Hilbert action. The module does not attach a physical polarization normalization.

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: