Gravity Analysis Edge Ttdecomposition4 D Decoy Projection Restores Transverse

The transverse trick

A transverse-traceless (TT) matrix is a symmetric grid of numbers whose trace, the sum of its diagonal entries, is zero, and whose product with a chosen wave vector is zero in every component. Such matrices describe the two independent polarizations of a gravitational wave in four dimensions. The theorem decoy_projection_restores_transverse concerns a specific matrix called decoyLongitudinal, built from a wave vector pointing along the first axis. This matrix is symmetric but deliberately not transverse: it fails the wave-vector condition by design.

The theorem states that after applying the standard TT projection, ttProject, to this decoy matrix, the result becomes transverse with respect to the axis wave vector. In other words, the projection repairs the defect. The proof is a direct consequence of a more general result, ttProject_isTT, which guarantees that the projection always yields a symmetric, traceless, and transverse matrix whenever the wave vector has nonzero squared length. The theorem is verified in the machine-checked library of formal theorems, with no unproved assumptions, and its axiom footprint is limited to the three standard logical axioms.

The same file proves a companion statement, decoyLongitudinal_not_transverse, confirming that the decoy matrix is genuinely not transverse before projection. Together these two results show that the projection does real work: it takes a matrix that fails the physical condition and produces one that satisfies it. The construction is purely algebraic, using the Euclidean trace and the standard dot product on four-dimensional real vectors, and it does not rely on any special choice of coordinates beyond the axis wave vector.

The theorem does not claim anything about the full theory of gravity. It does not decompose Regge edge perturbations on a four-dimensional lattice, does not prove convergence to the Einstein-Hilbert action, and does not address the Lorentzian or Minkowski case. The wave vector is Euclidean and nonzero; the theorem explicitly records that the decomposition hypothesis fails when the wave vector is zero, since the projection formula divides by the squared momentum. The result is a self-contained algebraic fact, not a statement about physical spacetime.

theorem decoy_projection_restores_transverse :
    IsTransverse axisWave (ttProject axisWave decoyLongitudinal) :=
  decoy_ttProject_isTT.2.2

theorem decoy_ttProject_isTT :
    IsTT axisWave (ttProject axisWave decoyLongitudinal) :=
  ttProject_isTT axisWave decoyLongitudinal decoyLongitudinal_symmetric
    (by simp [axisWave_momentumSq])

theorem decoyLongitudinal_not_transverse :
    ¬ IsTransverse axisWave decoyLongitudinal := by
  intro h
  have h0 := h 0
  simp [decoyLongitudinal, gaugePart, axisWave, Fin.sum_univ_four] at h0

What this page does not claim

This theorem does not decompose Regge edge perturbations on a 4D lattice. This theorem does not prove convergence to the Einstein-Hilbert action. This theorem does not address the Minkowski or Lorentzian case.

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: