Gravity Analysis Regge Bloch All Orbit Symbol4 D

The all-orbit symbol

Regge calculus is a way of doing general relativity without a smooth spacetime. Instead of a continuous manifold, one builds space from flat four-dimensional blocks glued together along their triangular faces, or hinges. The curvature lives at these hinges, where the sum of the angles of the blocks meeting there differs from the flat value. This gravity analysis examines a specific construction called the Bloch symbol, which encodes how a small perturbation with a given momentum behaves in such a discrete setting.

The central object is the all-orbit fold. The six types of hinges in a four-simplex can be grouped into four orbits under the symmetries of the structure. The construction defines a fold that sums contributions from all these orbits, using the area of each hinge and a deficit kernel that measures the curvature. A key property, proved in the library, is that this fold is even: reversing the direction of the momentum leaves the result unchanged. At zero momentum, the fold reduces to a simple quadratic form, and for two special configurations, the axis and a gauge mode, this quadratic form vanishes.

The construction also defines a second moment polynomial, which captures the leading behavior of the fold at small momenta. A theorem proves that if the area vector for an orbit is zero, this polynomial vanishes for that orbit. The library also records a warning: the symbol built from only one orbit does not match the target continuum value, so the full all-orbit sum is necessary. The construction explicitly does not prove that this discrete model recovers the Einstein-Hilbert action in the continuum limit, nor does it settle a related question about a gap action.

What this establishes in plain language is a precise, machine-checked vocabulary for talking about how this discrete gravity model responds to perturbations. It proves structural facts about the fold, like its evenness and its behavior at zero momentum, and it flags exactly which questions remain open. The library's status record marks two properties as false: the claim that the second moment tends to a limit for any direction is not yet closed for a single orbit, nor for the sum over all orbits. This is an honest inventory of what is known and what is not.

theorem foldAllAlong_even (H : Mat4) (dir : Fin 4 → ℝ) :
    Function.Even (foldAllAlong H dir) :=
  fun μ => foldAllAlong_neg H dir μ

theorem foldAllAlong_zero (H : Mat4) (dir : Fin 4 → ℝ) :
    foldAllAlong H dir 0 = trueWeightZeroMomQuadratic H := by
  unfold foldAllAlong
  simp_rw [zero_smul_dir]
  exact factorizedBlochFoldAll_zeroMomentum H

theorem foldAllAlong_axis_zero (dir : Fin 4 → ℝ) :
    foldAllAlong axisTTPlus dir 0 = 0 := by
  rw [foldAllAlong_zero, trueWeightZeroMomQuadratic_axisTTPlus]

theorem foldAllAlong_gauge_zero (dir : Fin 4 → ℝ) :
    foldAllAlong decoyGauge dir 0 = 0 := by
  rw [foldAllAlong_zero, trueWeightZeroMomQuadratic_decoyGauge]

/-- At vanishing area·H the moment polynomial is identically zero. -/
theorem m2OrbitMomentPoly_of_area_zero (ty : HingeOrbitType) (H : Mat4)
    (dir : Fin 4 → ℝ) (hA : classDot (orbitAreaCov ty) H = 0) :
    m2OrbitMomentPoly ty H dir = 0 := by
  unfold m2OrbitMomentPoly
  refine Finset.sum_eq_zero fun s _ => Finset.sum_eq_zero fun t _ => ?_
  by_cases ht : isOrbit ty s t <;> simp [ht, hA]

/-- Named OPEN props remain uninhabited status markers (not theorems). -/
theorem open_props_are_status_false :
    blochAllOrbitSymbol4DStatus.orbitM2TendstoClosed = false ∧
      blochAllOrbitSymbol4DStatus.allOrbitM2TendstoClosed = false := by
  decide

What this page does not claim

This module does not prove continuum Einstein-Hilbert recovery. This module does not flip the gap action recovery status. A one-orbit symbol is not equal to the continuum target.

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