pairwise_shared_tets
plain-language theorem explainer
Each pair among three 4-simplices on six vertices meets in a 4-vertex tetrahedron that contains the shared hinge triangle, so the gluing is face-to-face around that hinge. Researchers auditing the minimal interior-hinge complex in the SevenGaps/Regge gravity stack cite this as the combinatorial gluing fact. The proof is a pure finite-set decision: `decide` on explicit Finset equalities and inclusions.
Claim. Let $A=\{0,1,2,3,4\}$, $B=\{0,1,2,4,5\}$, $C=\{0,1,2,3,5\}$ be three 4-simplices on vertex set $\mathrm{Fin}\,6$, and let $H=\{0,1,2\}$ be the hinge triangle. Then $A\cap B=\{0,1,2,4\}$ with $|A\cap B|=4$ and $H\subseteq A\cap B$; $B\cap C=\{0,1,2,5\}$ with $|B\cap C|=4$ and $H\subseteq B\cap C$; and $A\cap C=\{0,1,2,3\}$ with $|A\cap C|=4$ and $H\subseteq A\cap C$.
background
The three-pent interior hinge witness builds the minimal simplicial complex whose hinge link is a cycle. Three 4-simplices ("pents") sit on Fin 6 and all contain the hinge triangle $H={0,1,2}$ imported from the two-pent glued-pents module: $A={0,1,2,3,4}$ (residual pair ${3,4}$), $B={0,1,2,4,5}$ (residual ${4,5}$), $C={0,1,2,3,5}$ (residual ${3,5}$).
The module is the positive half of a gate (panel P1-remainder, live bet C12) deciding whether glued-pent expressions may be called Regge action. The committed two-pent path witness already shows three pents are necessary for an interior hinge; this complex shows three suffice when glued face-to-face.
Face-to-face gluing means each adjacent pair shares exactly one tetrahedron of four vertices containing the hinge. The hinge itself is the 2-face ${0,1,2}$ of those shared tetrahedra (definition from the glued-pents hinge witness).
proof idea
The claim is a three-way conjunction of finite-set facts: explicit equality of each pairwise intersection, cardinality four, and hinge inclusion. The proof is a one-line decide. Lean unfolds the concrete Finset definitions of the three pents and the hinge on Fin 6, then the kernel decision procedure evaluates the equalities, card computations, and subset checks by brute-force computation. No intermediate lemmas are applied.
why it matters
This is the combinatorial gluing kernel of the three-pent complex that attains the lower bound of three pents for an interior hinge. The module doc names it (with its uniqueness sibling) as the witness that each adjacent pair shares exactly one tetrahedron containing the hinge, and that the triple intersection is exactly the hinge. Later facts in the same module (residual link edges, link vertex set ${3,4,5}$, edge triangle $3{-}4{-}5{-}3$, degree-two vertices, and the statements that the hinge is a genuine interior hinge and that the configuration is minimal) rest on this face-to-face structure.
In the Gravity/SevenGaps stack it supplies the positive half of the interior-hinge gate for treating glued-pent expressions as Regge action, complementing the counting lemma that three pents are necessary. It is pure discrete geometry: no appeal to the forcing chain T0–T8, the RCL, or continuum curvature values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.