Gravity Analysis Regge Hinge4 Dorbit Classification Realizable Matches Rep Orbit

The orbit classification

The declaration realizable_matches_rep_orbit is a formal theorem in the framework's machine-checked library of formal theorems. It concerns a four-dimensional cube, cut into 24 tetrahedral pieces called a Kuhn triangulation. Within this dissection, the theorem classifies every possible triangle hinge, a shared edge between two tetrahedra, by its shape and orientation. The result is purely combinatorial: it counts and sorts these hinges, and proves that the sorting is complete.

The classification works by representing each triangle's three vertices as bit masks, binary numbers that mark which of the cube's 16 corners the triangle touches. The theorem proves that every such triangle can be described by two disjoint difference masks, which record how the vertex set changes as you move along the triangle's edges. These masks come in exactly six types, determined by how many bits change at each step: (1,1), (1,2), (2,1), (1,3), (3,1), and (2,2). The proof counts the triangles of each type in a single cube: 72 of type (1,1), 48 each of types (1,2) and (2,1), and 24 each of the remaining three, for a total of 240 oriented triangle slots.

The theorem's main content is that these six types are exactly the orbits of a symmetry group. Permuting the four coordinate axes of the cube preserves the type of a triangle, and the proof shows this action is transitive: within each type, any triangle can be reached from any other by some coordinate permutation. A further symmetry, bitwise complement (swapping each corner with its opposite), merges pairs of types, reducing the six orbits to four. The declaration also establishes that a decoy pair of overlapping masks, type (1,3), is not realizable as a triangle hinge, ruling out a tempting false classification.

In Recognition Science, this result is a prerequisite for a larger goal: assembling the flat Hessian, a matrix of second derivatives, for the four-dimensional Regge action, a discrete version of Einstein's equations. The classification organizes the building blocks so that the Hessian can be assembled from per-orbit kernels. The theorem is kernel-checked, meaning it is proved with no gaps, no admitted axioms, and no shortcuts, and it relies only on the standard three axioms of the ambient type theory.

What the declaration does not do is equally precise. It does not evaluate the actual numerical kernels attached to each orbit, beyond a seed case. It does not complete the flat Hessian, nor does it prove that the discrete action converges to the continuous Einstein-Hilbert action in four dimensions. It does not establish any physical claim about gravity itself. The theorem is a combinatorial classification, a complete inventory of shapes, not a statement about the dynamics those shapes will eventually support.

/-- 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 orbit_count_S4 : Fintype.card HingeOrbitType = 6 := by
  decide

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

/-- THEOREM (decoy): overlapping masks `(1,3)` are not a monotone
difference pair. -/
theorem decoy_overlapping_not_realizable :
    isRealizableDiffPair 1 3 = false := by
  decide

What this page does not claim

The declaration does not evaluate any per-orbit star kernel beyond the seed orbit. The declaration does not complete the flat Hessian of the 4D Regge action. The declaration does not prove convergence of the discrete action to the Einstein-Hilbert action, nor does it make any physical claim about gravity.

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: