Gravity Analysis Edge Ttdecomposition4 D Euclidean Trace Transverse Projector

The transverse projector

In the study of gravitational waves, physicists often split a small perturbation of spacetime into pieces with different meanings. One piece, the transverse part, points perpendicular to the direction the wave travels. Another piece, the traceless part, carries no overall expansion or contraction. Together they form the transverse-traceless (TT) gauge, the standard way to describe the two physical polarizations of a gravitational wave in general relativity.

The declaration euclideanTrace_transverseProjector belongs to a machine-checked library of formal theorems, a collection of mathematical statements verified step by step by a computer. The declaration itself is a definition, not a theorem: it names a specific matrix called the transverse projector, a matrix that, when applied to another matrix, removes the part pointing along a chosen direction. The formula is P = 1 - m mᵀ / (m · m), where m is a nonzero four-component vector representing the wave direction. The identity matrix 1 and the outer product m mᵀ are both 4 × 4 real matrices.

The surrounding file proves that this projector has the properties its name promises. It is symmetric, meaning Pᵢⱼ = Pⱼᵢ for all indices i and j. It is transverse with respect to m, meaning P applied to m gives zero. And it is idempotent, meaning applying it twice gives the same result as applying it once. These three facts together establish that the transverse projector is a genuine projection operator onto the subspace of matrices perpendicular to m.

The file also constructs two explicit matrices, called axisTTPlus and axisTTCross, that are both transverse and traceless with respect to the axis direction m = (1,0,0,0). These are the two independent polarizations expected in four dimensions. The theorems prove that both are nonzero and that they are distinct, confirming that the TT subspace has at least two dimensions.

What the declaration does not claim is equally important. It does not decompose actual gravitational perturbations on a four-dimensional lattice, which would require a discrete version of the Einstein equations. It does not prove that the full action of the framework's theory converges to the Einstein-Hilbert action in four dimensions. And it does not apply to Lorentzian or null vectors, only to Euclidean ones. The file explicitly defers the Minkowski/null specialization for the Lorentzian continuum. The transverse projector is a linear-algebra tool, not a complete theory of gravity.

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

theorem outerSq_symmetric (m : Fin 4 → ℝ) :
    IsSymmetric (outerSq m) := by
  intro i j; unfold outerSq; ring

theorem axisTTPlus_ne_zero : axisTTPlus ≠ 0 := by
  intro h
  have := congrArg (fun M : Mat4 => M 2 2) h
  simp [axisTTPlus] at this

What this page does not claim

The declaration does not decompose Regge edge perturbations on a 4D lattice. The declaration does not prove that the framework's action converges to the Einstein-Hilbert action in four dimensions. The declaration does not apply to Lorentzian or null vectors, only to Euclidean ones.

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