Gravity Analysis Regge Hinge4 Dorbit Classification Decoy Overlapping Is Not Dis

The overlapping decoy

In four-dimensional geometry, a hinge is the shared edge where two triangles meet, like the crease where two pages of a folded paper model touch. The framework's gravity program studies these hinges inside a standard four-dimensional cube, cut into 24 tetrahedral pieces called Kuhn simplices. Each triangle in this dissection can be described by the corner points it touches, and the classification task is to sort all 240 possible oriented triangles into a small number of types by how their corner sets differ.

The declaration decoy_overlapping_is_not_disjoint settles a specific trap in that sorting task. A pair of difference masks, which record which corner positions change as you move from one vertex of a triangle to the next, is called disjoint when the two masks have no bits in common. The pair (1,3) looks promising at first glance: the numbers 1 and 3 have different bit patterns, so one might guess they represent a valid, non-overlapping pair. The theorem proves this guess wrong. The machine-checked result states that isDisjointDiffPair 1 3 = false, meaning the pair is not disjoint, and a companion theorem shows it is not realizable as an actual triangle difference pair at all.

Why does this matter? The whole point of the classification is to group triangles by their difference-mask types, and the framework's library proves that exactly six such types occur: (1,1), (1,2), (2,1), (1,3), (3,1), and (2,2). The pair (1,3) is a decoy because it appears in that list of types, but the specific masks 1 and 3 overlap in a way that makes them unusable as a difference pair. The theorem blocks a false shortcut: without it, a researcher might try to use (1,3) as a representative of its type and build a wrong orbit classification. The proof is a simple finite check, but it is a kernel-checked one, with no gaps and no extra axioms.

What the theorem does not claim is just as important. It does not say anything about the physical content of gravity, the Regge action, or whether the framework's action converges to the Einstein-Hilbert action in four dimensions. It is purely combinatorial, a gate that keeps the classification honest. The library's own documentation lists what remains open: the flat Hessian of the 4D Regge action is not completed, and the convergence result S_RS_converges_EH_4d is not proved. The decoy theorem is a necessary cleanup step, not a physical discovery.

theorem decoy_overlapping_is_not_disjoint :
    isDisjointDiffPair 1 3 = false := 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

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

What this page does not claim

The theorem does not prove anything about the physical Regge action or its convergence to Einstein-Hilbert gravity. The theorem does not claim that all pairs with overlapping bits are invalid, only that the specific pair (1,3) is not disjoint. The theorem does not complete the classification of absolute triangle positions within a single 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: