Gravity Analysis Edge Ttdecomposition Lorentz4 D Lorentz Load Gauge Part Gauge V

The gauge subtraction

In general relativity, a small perturbation of the metric is not unique. You can change coordinates, and the perturbation changes in a way that carries no physical information. The part that changes under such a coordinate shift is called the gauge part. The declaration lorentzLoad_gaugePart_gaugeVector is a definition inside the framework's machine-checked library of formal theorems: it names the specific object that gets subtracted away when a perturbation is cleaned of gauge freedom.

The setup is four-dimensional spacetime with the standard Minkowski metric of signature (-,+,+,+), where time enters with a minus sign. A wave is described by a covector, a direction in spacetime. The gauge part is built from that wave direction and a second vector, the gauge vector, by a symmetrized product: for each pair of indices, it is the sum of the products of the two vectors' components, swapped. This is exactly the algebraic shape of an infinitesimal coordinate transformation acting on a metric perturbation. The declaration defines this gauge part as a function of the wave and the gauge vector, nothing more.

The library proves that this gauge part is symmetric, a property any metric perturbation must have. It also proves that the gauge part is transverse to the wave direction in the Lorentzian sense, meaning its contraction with the raised wave covector vanishes. These two facts, symmetry and transversality, are what make the gauge part a legitimate candidate for subtraction: removing it preserves the symmetric, transverse character of the physical remainder.

What the declaration does not do is as important as what it does. It does not assert that any particular perturbation is physical or unphysical. It does not choose a gauge, nor does it prove that the subtraction removes all gauge freedom. It does not assign a physical polarization normalization to the wave. It does not claim that the transverse-traceless decomposition of a perturbation on a four-dimensional lattice converges to the Einstein-Hilbert action. Those are separate results, some proved elsewhere in the library and some still open. The declaration is a single algebraic tool: the definition of the gauge part, ready to be used in a larger decomposition.

def gaugePart (m v : Fin 4 → ℝ) : Mat4 :=
  fun i j => m i * v j + v i * m j

theorem gaugePart_symmetric (m v : Fin 4 → ℝ) :
    IsSymmetric (gaugePart m v) := by
  intro i j; unfold gaugePart; ring

What this page does not claim

The declaration does not prove that any perturbation is physical or unphysical. It does not assign a physical polarization normalization to the wave. It does not claim that the transverse-traceless decomposition converges to the Einstein-Hilbert action.

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: