Gravity Analysis Regge4 Dtensor Algebraic Closer

The 4D closure status

Regge calculus discretizes spacetime into flat 4-simplices, with curvature concentrated on triangular hinges. The ledger here is a discrete record of these hinge contributions. In four dimensions, the Regge action sums over these hinges, and its continuum limit should reproduce the Einstein-Hilbert action of general relativity. The module Regge4DTensorAlgebraicCloser tracks how far a specific algebraic identity, the 4D counterpart of a known 3D result, has been proven.

In three dimensions, a clean tensor identity closes the algebra: a certain quadratic form equals a universal contraction, written as K = (1/2) xᵀ adj(E) x = -(1/4)|x|²‖E‖_F². This 4D module banks progress toward the analogous 4D identity. It proves a homogeneity property: scaling the polarization E by a constant c scales the distinct-hinge moment m² by c². It also evaluates the moment on specific rays, such as the plus and cross polarization modes, yielding values like -1/4 and -1/8. These ray evaluations are banked as theorems in the machine-checked library.

The module also records an arithmetic residual. On a normalized ray, the distinct-hinge moment gives -1/16, while the Einstein-Hilbert coefficient is -1/4, a factor of 4 apart. The module proves this arithmetic fact, but the geometric reason for this factor, possibly from a Schläfli identity, remains open. The status structure lists what is closed and what is open: ray evaluations banked, homogeneity closed, tensor closed form open, factor-4 geometric closure open, axis isotropy blocked, and gap action recovery not flipped.

The practical consequence is a precise map of what is known. A reader can see that the 4D algebraic closer has not yet achieved the elegant closed form of its 3D predecessor. The open problems are named as targets, not impossibilities. The module does not install a magic factor of 4, and it does not claim the full tensor identity. It provides a checkpoint for future work on the discrete-to-continuum bridge in 4D Regge gravity.

theorem distinctHingeMomentForm_smul (c : ℝ) (E : Mat4) (dir : Fin 4 → ℝ) :
    distinctHingeMomentForm (c • E) dir =
      c ^ 2 * distinctHingeMomentForm E dir :=
  m2TransportedAllOrbitMomentDistinctHinge_smul c E dir

theorem distinctHingeMomentForm_axisTTPlus_symbolDir :
    distinctHingeMomentForm axisTTPlus symbolDir = (-1 / 4 : ℝ) :=
  m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_symbolDir

theorem distinctHingeMomentForm_axisTTCross_e0Dir :
    distinctHingeMomentForm axisTTCross e0Dir = (-1 / 8 : ℝ) :=
  m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_e0Dir

/-- Arithmetic residual (THEOREM side): pinned continuum face vs EH. -/
theorem residual_factor_four_arithmetic :
    einsteinHilbertTTCoefficient4D = (4 : ℝ) * (-1 / 16 : ℝ) ∧
      DistinctHingePinnedMomentVsEH ∧
        survivingDictionaryFactor4D = 1 :=
  ⟨by rw [einsteinHilbertTTCoefficient4D_eq]; norm_num,
    distinctHinge_pinned_ne_eh, rfl⟩

What this page does not claim

The full 4D tensor closed form is not proven; it is a named open target. The geometric origin of the factor 4 is not established. The module does not derive the Einstein-Hilbert action from Regge calculus; it banks partial algebraic results.

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