Gravity Analysis Regge Edge Ttattachment4 D Residual Trace Eq Zero Of Is Tt

The residual trace vanishes

In the four-dimensional lattice gravity analysis, a symmetric matrix H can be split into three parts: a transverse-traceless part, a gauge part, and a residual trace part. The declaration residualTrace_eq_zero_of_isTT states that if H is transverse and traceless (with nonzero momentum), then its residual trace part is exactly zero. This is a proved theorem in the machine-checked library of formal theorems, with no axioms beyond the standard three.

The proof unfolds the definition of the residual trace, uses the fact that the gauge-corrected matrix equals H, and applies the traceless condition. The result is a clean algebraic identity: the residual trace part vanishes identically. This is not a numerical approximation; it is an exact equality in the formal system.

What this does not claim is broader. It does not prove that the full edge TT decomposition works in four dimensions, nor that the Regge action recovers Einstein-Hilbert in the continuum. It does not establish any physical result about gravity. It is a technical lemma within a larger program, one step in a chain that remains incomplete.

theorem residualTrace_eq_zero_of_isTT (m : Fin 4 → ℝ) (H : Mat4)
    (hTT : IsTT m H) (hm : momentumSq m ≠ 0) :
    residualTrace m H = 0 := by
  unfold residualTrace
  rw [gaugeCorrected_eq_of_isTT m H hTT hm]
  have := hTT.2.1
  simp [IsTraceless] at this
  simp [this]

What this page does not claim

This does not prove the full edge TT decomposition in four dimensions. This does not prove that the Regge action recovers Einstein-Hilbert in the continuum. This does not establish any physical result about gravity.

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