Gravity Analysis Regge Hinge4 Dorbit Classification Hinge4 Dorbit Classification

Classifying triangle hinges

In four-dimensional geometry, a simplex is the simplest shape: a point, a line, a triangle, a tetrahedron, or a 4-simplex. When physicists discretize spacetime for numerical work, they often chop a 4-cube into 24 such 4-simplices, called Kuhn simplices. Each 4-simplex contains ten triangular faces, and each triangle is a hinge where two 4-simplices meet. The declaration hinge4DOrbitClassificationStatus_flags is a machine-checked classification of all 240 oriented triangle slots that appear in one unit 4-cube, sorted by how their vertices differ.

The classification works by labeling each vertex of the cube with a 4-bit mask, a string of four zeros and ones. A triangle's three vertices form a chain of masks, and the differences between successive masks are themselves masks. The type of a triangle is the pair of numbers of nonzero bits in those two difference masks. The proof shows that every triangle falls into one of six types, with counts 72, 48, 48, 24, 24, and 24. Under symmetries that permute the four coordinate axes, these six types are the only distinct orbits. Adding a complement symmetry, which flips all bits, merges some types and leaves four orbits.

The proof is combinatorial only. It does not evaluate any physical kernel, does not complete the flat Hessian of the 4D Regge action, and does not prove that the discrete action converges to general relativity. The declaration establishes a counting and symmetry result about abstract triangles in a cube, nothing more.

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

def orbitLocalSq : HingeOrbitType → OrbitLocalSq
  | ty => localSqOfDiff (orbitRep ty).1 (orbitRep ty).2

What this page does not claim

The declaration proves that the discrete Regge action converges to general relativity. The declaration evaluates the physical star kernels that contribute to the Hessian. The declaration classifies tetrahedra or 4-simplices, only triangles.

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: