Gravity Analysis Regge Edge Ttattachment4 D Gauge Vector Eq Zero Of Is Tt

The gauge vector vanishes

In the Recognition Science framework's machine-checked library of formal theorems, a result named gaugeVector_eq_zero_of_isTT concerns a four-dimensional lattice model of gravity. The framework models spacetime as a discrete grid, and it studies small perturbations, or loadings, on the edges of this grid. A key object is a 4 by 4 matrix representing a perturbation. The theorem states that if this matrix satisfies a particular condition, denoted IsTT, then a specific vector, the gauge vector, is identically zero.

The condition IsTT is a conjunction of two properties: the matrix is traceless, meaning the sum of its diagonal entries is zero, and it is transverse, meaning it is orthogonal to the wave covector that defines the plane-wave perturbation. The theorem is a formal consequence of the definitions and earlier lemmas in the library. It is proved in the Lean 4 proof assistant, with the expected axiom footprint limited to the standard three axioms [propext, Classical.choice, Quot.sound]. This means the result is a theorem in the strictest sense, not a hypothesis or a modeling choice.

The practical content of the theorem is that for a perturbation that is already transverse and traceless, the gauge-fixing vector, which is used to remove redundant degrees of freedom, carries no additional information. This is a technical but necessary step in the framework's program to decompose any perturbation into a transverse-traceless part, a gauge part, and a residual trace part. The theorem ensures that this decomposition is well-defined and that the gauge part vanishes for the physically relevant class of perturbations.

What the theorem does not claim is broader physical significance. It does not prove that the full ledger name edge_tt_decomposition is realized, meaning it does not establish the complete 4D Regge action, nor does it recover the continuum Einstein-Hilbert action from the lattice model. It also does not prove the convergence of the framework's action to the Einstein-Hilbert action in four dimensions, and it does not flip the status of the gap_action_recovery property. These remain open targets within the framework, not achievements of this particular theorem.

theorem load_eq_zero_of_isTT (m : Fin 4 → ℝ) (H : Mat4) (h : IsTT m H)
    (i : Fin 4) : load H m i = 0 :=
  h.2.2 i

theorem gaugeCorrected_eq_of_isTT (m : Fin 4 → ℝ) (H : Mat4)
    (hTT : IsTT m H) (hm : momentumSq m ≠ 0) :
    gaugeCorrected m H = H := by
  unfold gaugeCorrected
  rw [gaugeVector_eq_zero_of_isTT m H hTT hm, gaugePart_zero]
  simp

theorem load_eq_zero_of_isTT (m : Fin 4 → ℝ) (H : Mat4) (h : IsTT m H)
    (i : Fin 4) : load H m i = 0 :=
  h.2.2 i

What this page does not claim

This theorem does not prove the full 4D Regge action or continuum Einstein-Hilbert recovery. This theorem does not establish the convergence of the framework's action to the Einstein-Hilbert action. This theorem does not prove that the ledger name edge_tt_decomposition is realized in full.

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: