Gravity Analysis Regge Hinge4 Dorbit Classification Complement Swaps Diff Pair

Complement symmetry

In the four-dimensional cube, a triangle is defined by three vertices. The Recognition Science framework's machine-checked library of formal theorems examines these triangles by encoding each vertex as a four-bit mask, a string of four zeros and ones that marks which coordinates are present. The declaration complement_swaps_diff_pair concerns the operation of flipping every bit in such a mask, turning zeros into ones and vice versa. This operation, called bitwise complement, sends each vertex to its opposite corner in the cube.

The theorem proves that this complement operation preserves the set of valid triangles: applying it to any triangle in the cube yields another triangle in the cube. More specifically, it swaps the two numbers that describe how the triangle's vertices differ from one another. Each triangle has a type, a pair of counts (i, j) recording how many new coordinates appear at each step as you move from one vertex to the next. The complement operation exchanges these two counts, turning a triangle of type (1, 2) into one of type (2, 1), and similarly for (1, 3) and (3, 1). Types (1, 1) and (2, 2) remain unchanged, since swapping equal numbers changes nothing.

This symmetry has a concrete consequence. When the framework classifies triangles by their shape up to coordinate permutation, it finds six distinct classes. Adding the complement operation merges pairs of these classes, reducing the count to four. This is a purely combinatorial fact about the geometry of the four-dimensional cube, established by exhaustive case analysis in the machine-checked library. It is a stepping stone toward a larger goal: assembling the full curvature expression for a four-dimensional spacetime in a discrete, combinatorial setting.

The declaration does not claim anything about physics. It does not compute any physical quantity, does not evaluate the curvature of any specific triangle, and does not prove that the discrete theory converges to Einstein's equations in four dimensions. It is a statement about the symmetries of triangles in a single four-dimensional cube, nothing more and nothing less.

/-- Bitwise complement inside the unit 4-cube. -/
def complementMask (m : ℕ) : ℕ := Nat.xor m 15

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

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

What this page does not claim

The declaration does not evaluate any physical quantity or curvature. The declaration does not prove convergence to Einstein's equations in four dimensions. The declaration does not concern triangles outside a single four-dimensional cube.

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: