Gravity Analysis Regge Edge Ttattachment4 D

A lattice gravity step

General relativity describes gravity as the curvature of spacetime, a smooth continuous fabric. A major open problem in physics is how this smooth picture emerges from a more fundamental, discrete reality. One approach, lattice gravity, replaces continuous spacetime with a grid of points, and the equations of motion with finite differences. The module in question is a small but rigorously checked piece of this programme: it proves that a standard mathematical decomposition of the gravitational field, the transverse-traceless (TT) split, works correctly when applied to simple plane-wave disturbances on a four-dimensional lattice.

The TT split is a way of separating a gravitational field into independent parts: a physical, propagating part (the TT part), a part that is pure coordinate choice (the gauge part), and a residual trace part. The module proves that on a four-dimensional lattice, the total effect of a plane-wave perturbation on the length of a lattice edge is exactly the sum of the effects of these three parts. This is a linearity property, and it is a prerequisite for isolating the physical degrees of freedom from the coordinate artifacts in a discrete setting.

More specifically, the module proves an exact lattice identity for the gauge part. In the continuum, a gauge transformation changes the metric by a derivative of a vector field. On the lattice, the module shows that the gauge part of the edge perturbation is exactly proportional to a discrete version of this derivative, a finite difference of a sine wave. This is not an approximation; it is an exact algebraic identity on the lattice, and it is the correct discrete analogue of the continuum statement.

In Recognition Science, this is one step in a larger campaign to derive the Einstein-Hilbert action, the mathematical expression that gives Einstein's field equations, from the framework's foundational concept of a ledger, a discrete record of events. The module does not achieve that goal. It does not prove the full Einstein-Hilbert recovery, nor does it prove that the framework's action converges to it. What it does establish is a necessary technical lemma: that the TT decomposition behaves correctly on the lattice for plane waves, with the gauge part matching a discrete Lie derivative. This is a concrete, verified piece of the bridge between a discrete starting point and continuous gravity.

The practical consequence is that the framework's path to gravity has a solid, checked foundation for this specific operation. The proof is machine-checked, meaning a computer program has verified every logical step, with no gaps and no additional assumptions beyond the standard logical axioms. This gives researchers a reliable building block to use in further work, rather than a heuristic argument that might fail under scrutiny.

theorem planeWaveAxisEdgePert_decomposition (m : Fin 4 → ℝ) (H : Mat4)
    (hH : IsSymmetric H) (hm : momentumSq m ≠ 0) (x : Fin 4 → ℝ)
    (a : Fin 4) :
    planeWaveAxisEdgePert H m x a =
      planeWaveAxisEdgePert (ttProject m H) m x a +
        planeWaveAxisEdgePert (gaugePart m (gaugeVector m H)) m x a +
        planeWaveAxisEdgePert (residualTrace m H • transverseProjector m)
          m x a := by
  unfold planeWaveAxisEdgePert
  rw [edgeLoad_decomposition m H hH hm]
  ring

/-- Plane-wave edge perturbation of a gauge matrix on an axis edge. -/
theorem planeWaveAxisEdgePert_gaugePart (m v x : Fin 4 → ℝ) (a : Fin 4) :
    planeWaveAxisEdgePert (gaugePart m v) m x a =
      2 * m a * v a * Real.cos (axisMidpointPhase m x a) := by
  unfold planeWaveAxisEdgePert
  rw [edgeLoad_gaugePart_axis]

What this page does not claim

This module does not prove the full Einstein-Hilbert action recovery. This module does not prove that the framework's action converges to the Einstein-Hilbert action. This module does not establish the physical bridge between the discrete ledger and continuous 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/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: