Gravity Analysis Edge Ttdecomposition4 D Gauge Corrected Transverse

The gauge correction

In general relativity, gravitational waves are described by perturbations of the spacetime metric. A standard way to isolate the physical degrees of freedom is to demand that the perturbation be transverse and traceless: orthogonal to the direction of wave propagation, and with zero sum of diagonal entries. In four dimensions, this leaves exactly two independent polarization states, the familiar plus and cross modes.

The declaration gaugeCorrected_transverse is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It proves, for a symmetric 4 by 4 real matrix representing a perturbation, that the operation called gauge correction (a subtraction of a term built from the wave direction) produces a matrix that is transverse to that direction. The theorem is part of a linear-algebra layer: it works with Euclidean trace and transversality, and it does not yet handle the Minkowski or null case needed for the Lorentzian continuum.

The proof is fully formalized and kernel-checked, with no gaps and no extra axioms beyond the three standard ones of the ambient type theory. The library also proves that the full transverse-traceless projection of a symmetric matrix is symmetric, traceless, and transverse, and that the projection of a deliberately longitudinal test matrix restores transversality. These results establish the algebraic machinery for isolating the two independent polarization states on a chosen axis wave vector.

What the declaration does not claim is equally important. It does not decompose Regge edge perturbations on a 4D lattice, does not prove convergence to the Einstein-Hilbert action, and does not handle the Minkowski signature needed for physical spacetime. The theorem is a precise algebraic statement, not a physical derivation.

def gaugeCorrected (m : Fin 4 → ℝ) (H : Mat4) : Mat4 :=
  H - gaugePart m (gaugeVector m H)

def gaugeCorrected (m : Fin 4 → ℝ) (H : Mat4) : Mat4 :=
  H - gaugePart m (gaugeVector m H)

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

What this page does not claim

The declaration does not decompose Regge edge perturbations on a 4D lattice. The declaration does not prove convergence to the Einstein-Hilbert action. The declaration does not handle the Minkowski signature needed for physical spacetime.

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: