Gravity Analysis Regge Hinge4 Dorbit Classification

Classifying the hinges

Regge calculus is a way to do general relativity without continuous spacetime. Spacetime is chopped into flat blocks, like a crystal, and gravity lives on the edges and hinges where the blocks meet. In four dimensions, the hinges are triangles. The Regge action, the discrete stand-in for Einstein's equations, sums a contribution from each triangle. Before that sum can be computed efficiently, the possible kinds of triangles must be known. This gravity analysis, the framework's study of how discrete geometry gives rise to gravitational structure, performs exactly that census.

The setting is one unit four-dimensional cube, split into the standard 24 tetrahedral pieces called a Kuhn triangulation. Each triangle in that triangulation is described by three vertex masks, bit patterns that say which of the cube's 16 corners the triangle touches. The classification establishes that every such triangle has a type: a pair of numbers (|a|,|b|) that counts how many new corners each edge of the triangle adds. The possible types are (1,1), (1,2), (2,1), (1,3), (3,1), and (2,2). It then counts them: there are 240 oriented triangle slots in the cube, and they split as 72, 48, 48, 24, 24, 24 across those six types.

The classification goes further. If the four coordinate axes of the cube are permuted, a triangle of one type can turn into another triangle of the same type. The classification proves that this permutation action is transitive on each type, meaning all triangles of a given type are equivalent up to relabeling the axes. That gives six orbits. If a complement symmetry is also allowed, which flips every corner of the cube to its opposite, the types (1,2) and (2,1) merge, and so do (1,3) and (3,1), leaving four orbits. The classification also records the local squared edge lengths for one representative of each of the six orbits, a package of numbers that later work can use.

In plain language, this classification is a sorting task. It takes every possible triangle hinge in a four-dimensional cube, groups them into a small number of families, and proves that the grouping is complete and correct. It does not compute the actual gravitational contribution of any hinge, and it does not assemble the full discrete Einstein equation. It is a combinatorial prerequisite, a necessary first step that the framework's library of machine-checked theorems has now completed.

The result matters because it turns an apparently infinite variety of geometric arrangements into a finite, small list. Any future calculation of the four-dimensional Regge action can be organized by these six orbit types, knowing that every triangle falls into exactly one family and that the families are closed under the symmetries of the cube. The classification is a piece of infrastructure: unglamorous, but load-bearing.

/-- THEOREM: every triangle slot has one of the six orbit types. -/
theorem hingeTypePop_is_orbitType (s : Fin 24) (t : Fin 10) :
    popToOrbitType (hingeTypePop s t) ≠ none := by
  fin_cases s <;> fin_cases t <;> decide

theorem oriented_slot_total :
    (Fintype.card (Fin 24) * Fintype.card (Fin 10)) = 240 := by
  decide

theorem cellTriangleCount_t11 : cellTriangleCount (1, 1) = 72 := by
  decide

theorem cellTriangleCount_t12 : cellTriangleCount (1, 2) = 48 := by
  decide

theorem cellTriangleCount_t21 : cellTriangleCount (2, 1) = 48 := by
  decide

theorem cellTriangleCount_t13 : cellTriangleCount (1, 3) = 24 := by
  decide

theorem cellTriangleCount_t31 : cellTriangleCount (3, 1) = 24 := by
  decide

theorem cellTriangleCount_t22 : cellTriangleCount (2, 2) = 24 := by
  decide

theorem orbit_count_S4 : Fintype.card HingeOrbitType = 6 := by
  decide

theorem orbit_count_S4_complement :
    Fintype.card HingeOrbitTypeModComplement = 4 := by
  decide

What this page does not claim

This module does not evaluate the per-orbit star kernels that give the actual gravitational contribution of each hinge. This module does not complete the flat Hessian of the four-dimensional Regge action. This module does not prove that the discrete Regge action converges to the Einstein-Hilbert action in four dimensions.

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