Gravity Analysis Regge Edge Stencil4 D

A finite stencil for gravity

Regge calculus is a way of doing general relativity without smooth geometry: spacetime is chopped into flat pieces, and gravity lives on the hinges and edges where those pieces meet. The module ReggeEdgeStencil4D is a step in that direction inside the Recognition Science framework. It studies how a small, plane-wave perturbation of the metric affects the edges of a four-dimensional hypercube, the 4D analogue of a cube. The work is a machine-checked collection of formal theorems, meaning every named result is verified by a proof assistant with no gaps.

The module first classifies the 15 nonzero displacement directions in a 4-cube, where each direction is a vector with entries 0 or 1. For each such direction, it computes a coefficient that measures how the perturbation loads that edge. The central object is a provisional finite quadratic form, written as the sum of squares of these coefficients over all 15 classes. This form is meant to approximate the true Regge Hessian, the matrix of second derivatives of the gravitational action, but with a simplification: every class is given equal weight 1.

That simplification is the honest limit of the module. The true 4D Regge weights, which would come from contracting the deficit angle with the hinge factor, are not derived here. The module states this openly: the correct weights remain an open problem and must not be reverse-engineered from the known Einstein-Hilbert answer. What the module does prove is that its provisional form behaves sensibly on certain test inputs. On a pure gauge perturbation, the form evaluates to 32; on a pure trace input, it evaluates to 80; and on a traceless-transverse seed, it is nonzero. These are concrete, checkable numbers.

The most important finding is negative. The provisional quadratic form is not gauge invariant: a pure gauge load, which should have no physical effect, produces a nonzero value. The module records the exact identity that holds instead, and gives an explicit counterexample. This is not a failure of the framework but a precise statement of what the provisional form can and cannot do. It tells a researcher that the equal-weight simplification is too crude for gauge invariance, and that the true weights must restore it.

In plain language, the module builds a toy model of gravity on a discrete 4D grid, checks how it responds to simple perturbations, and finds that the toy is not yet physical. It does not prove that this discrete gravity converges to Einstein's equations, and it does not claim to. What it establishes is a rigorous, machine-checked baseline: a finite stencil with known behavior on test inputs, and a clear, open target for the weights that would make it gauge invariant.

theorem classDisp_ne_zero (d : Fin 15) : classDisp d ≠ 0 := by
  intro h
  have hw := classWeightNat_pos d
  have hbits :
      classWeightNat d =
        (if classBit d 0 then 1 else 0) +
          (if classBit d 1 then 1 else 0) +
          (if classBit d 2 then 1 else 0) +
          (if classBit d 3 then 1 else 0) := rfl
  have hz : ∀ i : Fin 4, classDisp d i = 0 := by
    intro i; simp [h]
  have hb0 : classBit d 0 = false := by
    have := hz 0; simp [classDisp] at this; exact this
  have hb1 : classBit d 1 = false := by
    have := hz 1; simp [classDisp] at this; exact this
  have hb2 : classBit d 2 = false := by
    have := hz 2; simp [classDisp] at this; exact this
  have hb3 : classBit d 3 = false := by
    have := hz 3; simp [classDisp] at this; exact this
  simp [hbits, hb0, hb1, hb2, hb3] at hw

theorem finiteTTQuadratic_gaugePart_axisWave :
    finiteTTQuadratic (gaugePart axisWave axisGaugeVector) = 32 := by
  unfold finiteTTQuadratic
  have hterm :
      ∀ d : Fin 15,
        classCoeff (gaugePart axisWave axisGaugeVector) d ^ 2 =
          (4 : ℝ) * (hasBit0 d : ℝ) := by
    intro d
    rw [classCoeff_gaugePart_axis]
    unfold hasBit0
    cases classBit d 0 <;> norm_num
  simp_rw [hterm, ← Finset.mul_sum, ← Nat.cast_sum, sum_hasBit0]
  norm_num

theorem sum_weightSqNat : (∑ d : Fin 15, classWeightNat d ^ 2) = 80 := by
  unfold classWeightNat classBit maskOf
  decide

theorem finiteTTQuadratic_gaugePart_axisWave_ne_zero :
    finiteTTQuadratic (gaugePart axisWave axisGaugeVector) ≠ 0 := by
  rw [finiteTTQuadratic_gaugePart_axisWave]
  norm_num

What this page does not claim

This module does not prove convergence to the Einstein-Hilbert action in 4D. This module does not derive the true 4D Regge weights. This module does not establish exact gauge invariance for the provisional quadratic form.

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