Gravity Analysis Regge Hinge4 Dorbit Classification Absolute T11 Not S4 Transiti

What the orbit theorem proves

In the framework's discrete geometry of gravity, space is built from unit cubes, each cut into 24 tetrahedral cells by a standard triangulation. The declaration in question concerns the 240 oriented triangular faces that appear as hinges between these cells. The theorem establishes that the permutation group S₄, which rearranges the four coordinate axes, acts transitively on the six types of hinge orbits when hinges are classified by their difference masks: pairs of disjoint nonzero bitmasks that record how the triangle's vertices differ along the cube's edges. Each of the six types, labeled by popcount pairs such as (1,1) or (2,2), forms a single orbit under coordinate permutation, meaning any hinge of a given type can be mapped to any other hinge of that same type by some axis permutation.

The theorem's sharp edge is that this transitivity fails for absolute triangles within a single cube. A triangle's absolute placement, recorded as a triple of vertex masks, is not invariant under coordinate permutation in the same way. The vertex-popcount profiles distinguish positions, so two triangles of the same type can sit in inequivalent locations inside the cube. The classification therefore uses translation-normalized difference masks, not absolute placement, to achieve its six orbits. This distinction matters because the framework's next step, assembling a flat Hessian for the 4D Regge action, requires knowing which hinges are genuinely equivalent under the symmetries that preserve the triangulation.

The theorem also proves exact counts: 72 hinges of type (1,1), 48 each of types (1,2) and (2,1), and 24 each of types (1,3), (3,1), and (2,2), summing to the 240 oriented slots. Under the larger group that adds bitwise complement, which swaps type (i,j) with (j,i), the six orbits merge into four. The seed hinge {0, e₀, e₀+e₁} has type (1,1), and a decoy overlapping mask pair (1,3) is proved unrealizable, a gate that prevents a plausible but wrong classification.

What the declaration does not claim is equally precise. It does not evaluate per-orbit star kernels, does not complete the flat Hessian of the 4D Regge action, and does not prove convergence of the framework's action to the Einstein-Hilbert action in four dimensions. It is a combinatorial prerequisite, a piece of bookkeeping that must be correct before the physical assembly can proceed. The theorem's value is that it fixes the vocabulary of equivalence classes for one unit cube, so that later stages can speak of orbits rather than individual triangles.

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

/-- Absolute vertex-mask triple of a slot, as a sorted 3-tuple of `ℕ`. -/
def absoluteTriple (s : Fin 24) (t : Fin 10) : ℕ × ℕ × ℕ :=
  triangleVertexMasks s t

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 orbit_count_S4_complement :
    Fintype.card HingeOrbitTypeModComplement = 4 := by
  decide

What this page does not claim

This theorem does not evaluate per-orbit star kernels or complete the flat Hessian of the 4D Regge action. This theorem does not prove convergence of the framework's action to the Einstein-Hilbert action. The classification applies only to one unit 4-cube Kuhn triangulation, not to arbitrary lattices.

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: