Gravity Analysis Edge Ttdecomposition4 D Load Gauge Part Gauge Vector

The gauge correction identity

In the linear algebra of gravitational waves, a perturbation of the metric is a symmetric 4 by 4 matrix. Physical waves are transverse, meaning they carry no component along the direction of travel, and traceless, meaning their diagonal entries sum to zero. The framework's library, a machine-checked collection of formal theorems, works with these objects on a four-index vector space. Its declaration load_gaugePart_gaugeVector proves a specific algebraic identity: after applying the gauge correction, the load, or the matrix acting on a wave vector, returns exactly the original load.

To see what this means, consider a symmetric matrix H and a nonzero wave vector m. The gauge part is the symmetric matrix built from m and a second vector v. The gauge vector is a particular choice of v, constructed so that it cancels the unwanted longitudinal piece of H. The theorem states that when you apply the gauge correction, the load of the corrected matrix equals the load of the original matrix. In symbols, load(gaugePart m (gaugeVector m H)) m i = load H m i, for every index i. This is the algebraic heart of the transverse-traceless decomposition: it shows the gauge correction leaves the physical content of the wave untouched.

The identity is proved for a Euclidean wave covector on a four-dimensional space, with the standard trace and transversality conditions. It is a theorem in the framework's library, checked by the Lean kernel with no unproved assumptions. The declaration does not claim to decompose perturbations on a lattice, does not prove that the framework's action converges to the Einstein-Hilbert action in four dimensions, and does not address the Lorentzian or null case. Those remain open targets.

In the framework's account, this identity is a small but load-bearing step. It shows that the gauge correction is consistent: the corrected matrix carries the same load as the original, so the transverse-traceless projection is well-defined. The next step, the full projection theorem, builds on this foundation. For a reader, the practical lesson is that the gauge correction is not an arbitrary choice; it is forced by the requirement that the load be preserved.

theorem load_gaugePart_gaugeVector (m : Fin 4 → ℝ) (H : Mat4)
    (hm : momentumSq m ≠ 0) (i : Fin 4) :
    load (gaugePart m (gaugeVector m H)) m i = load H m i := by
  set w := load H m
  set s := momentumSq m
  set v := gaugeVector m H
  have hs0 : s ≠ 0 := hm
  have hL := load_gaugePart m v i
  have hdot := dot_gaugeVector m H hm
  have hvi : v i = w i / s - m i * dot w m / (2 * s ^ 2) := rfl
  have key : s * v i + m i * dot v m = w i := by
    rw [hvi, show dot v m = dot w m / (2 * s) from hdot]
    field_simp [hs0]; ring
  rw [hL]; simpa [s, w, v] using key

theorem load_gaugePart_gaugeVector (m : Fin 4 → ℝ) (H : Mat4)
    (hm : momentumSq m ≠ 0) (i : Fin 4) :
    load (gaugePart m (gaugeVector m H)) m i = load H m i := by
  set w := load H m
  set s := momentumSq m
  set v := gaugeVector m H
  have hs0 : s ≠ 0 := hm
  have hL := load_gaugePart m v i
  have hdot := dot_gaugeVector m H hm
  have hvi : v i = w i / s - m i * dot w m / (2 * s ^ 2) := rfl
  have key : s * v i + m i * dot v m = w i := by
    rw [hvi, show dot v m = dot w m / (2 * s) from hdot]
    field_simp [hs0]; ring
  rw [hL]; simpa [s, w, v] using key

What this page does not claim

The declaration does not decompose Regge EDGE perturbations on a 4D lattice. The declaration does not prove S_RS_converges_EH_4d. The declaration does not address the Minkowski or null specialization.

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: